menu

Return to entry

Utils
Nat_Miscellanea
ZF_Miscellanea
Renaming
Renaming_Auto
M_Basic_No_Repl
Eclose_Absolute
Recursion_Thms
Datatype_absolute
Internalize
Rec_Separation
Satisfies_absolute
DPow_absolute
Synthetic_Definition
Internalizations
Least
Higher_Order_Constructs
Relativization
Discipline_Base
Arities
Discipline_Function
Lambda_Replacement
Discipline_Cardinal
Univ_Relative
Cardinal_Relative
CardinalArith_Relative
Aleph_Relative
Cardinal_AC_Relative
FiniteFun_Relative
ZF_Library_Relative
Replacement_Lepoll
Cardinal_Library_Relative
Delta_System_Relative
Pointed_DC_Relative
Partial_Functions_Relative

Transitive_Models.Synthetic_Definition

HTML Presentation