FixedPointApproximants

📁 Source: Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

Statistics

Metric	Count
Definitions gfpApprox, lfpApprox	2
Theorems not_injective_limitation_set, exists_gfpApprox_eq_gfpApprox, exists_lfpApprox_eq_lfpApprox, gfpApprox_add_one, gfpApprox_antitone, gfpApprox_eq_of_mem_fixedPoints, gfpApprox_le, gfpApprox_mono_left, gfpApprox_mono_mid, gfpApprox_ord_eq_gfp, gfpApprox_ord_mem_fixedPoint, gfp_mem_range_gfpApprox, le_gfpApprox_of_mem_fixedPoints, le_lfpApprox, lfpApprox_add_one, lfpApprox_eq_of_mem_fixedPoints, lfpApprox_le_of_mem_fixedPoints, lfpApprox_mem_fixedPoints_of_eq, lfpApprox_mono_left, lfpApprox_mono_mid, lfpApprox_monotone, lfpApprox_ord_eq_lfp, lfpApprox_ord_mem_fixedPoint, lfp_mem_range_lfpApprox	24
Total	26

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_injective_limitation_set 📖	mathematical	—	Set.InjOn Ordinal Set.Iio PartialOrder.toPreorder Ordinal.partialOrder ord SuccOrder.succ Cardinal partialOrder instSuccOrder	—	lift_mk_le_lift_mk_of_injective Set.injOn_iff_injective card_ord Ordinal.mk_Iio_ordinal not_le_of_gt Order.lt_succ instNoMaxOrder lift_le lift_lift

OrdinalApprox

Definitions

Name	Category	Theorems
gfpApprox 📖	CompOp	11 math math: gfp_mem_range_gfpApprox, gfpApprox_ord_mem_fixedPoint, le_gfpApprox_of_mem_fixedPoints, gfpApprox_le, gfpApprox_add_one, gfpApprox_antitone, gfpApprox_ord_eq_gfp, exists_gfpApprox_eq_gfpApprox, gfpApprox_mono_mid, gfpApprox_mono_left, gfpApprox_eq_of_mem_fixedPoints
lfpApprox 📖	CompOp	12 math math: lfpApprox_mono_mid, lfpApprox_eq_of_mem_fixedPoints, lfpApprox_ord_eq_lfp, lfpApprox_le_of_mem_fixedPoints, lfpApprox_ord_mem_fixedPoint, lfpApprox_monotone, lfpApprox_add_one, lfpApprox_mono_left, lfpApprox_mem_fixedPoints_of_eq, exists_lfpApprox_eq_lfpApprox, lfp_mem_range_lfpApprox, le_lfpApprox

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_gfpApprox_eq_gfpApprox 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Cardinal.ord Order.succ Cardinal Cardinal.partialOrder Cardinal.instSuccOrder gfpApprox	—	exists_lfpApprox_eq_lfpApprox
exists_lfpApprox_eq_lfpApprox 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Cardinal.ord Order.succ Cardinal Cardinal.partialOrder Cardinal.instSuccOrder lfpApprox	—	Cardinal.not_injective_limitation_set Function.not_injective_iff Set.injOn_iff_injective Subtype.prop
gfpApprox_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike	gfpApprox Ordinal Ordinal.add Ordinal.one DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike	—	lfpApprox_add_one
gfpApprox_antitone 📖	mathematical	—	Antitone Ordinal PartialOrder.toPreorder Ordinal.partialOrder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder gfpApprox	—	lfpApprox_monotone
gfpApprox_eq_of_mem_fixedPoints 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike Ordinal Ordinal.partialOrder Set Set.instMembership Function.fixedPoints gfpApprox	gfpApprox	—	lfpApprox_eq_of_mem_fixedPoints
gfpApprox_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder gfpApprox	—	le_lfpApprox
gfpApprox_mono_left 📖	mathematical	—	Monotone OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder Pi.preorder Ordinal gfpApprox	—	lfpApprox_mono_left
gfpApprox_mono_mid 📖	mathematical	—	Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder Pi.preorder Ordinal gfpApprox	—	lfpApprox_mono_mid
gfpApprox_ord_eq_gfp 📖	mathematical	—	gfpApprox Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Cardinal.ord Order.succ Cardinal Cardinal.partialOrder Cardinal.instSuccOrder DFunLike.coe OrderHom OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.gfp	—	lfpApprox_ord_eq_lfp
gfpApprox_ord_mem_fixedPoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike	Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike gfpApprox Cardinal.ord Order.succ Cardinal Cardinal.partialOrder Cardinal.instSuccOrder	—	lfpApprox_ord_mem_fixedPoint
gfp_mem_range_gfpApprox 📖	mathematical	—	Set Set.instMembership Set.range Ordinal gfpApprox Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe OrderHom OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.gfp	—	lfp_mem_range_lfpApprox
le_gfpApprox_of_mem_fixedPoints 📖	mathematical	Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike Preorder.toLE	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder gfpApprox	—	lfpApprox_le_of_mem_fixedPoints
le_lfpApprox 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder lfpApprox	—	lfpApprox.eq_1 le_sSup Set.union_singleton
lfpApprox_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike	lfpApprox Ordinal Ordinal.add Ordinal.one DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike	—	le_antisymm lfpApprox.eq_1 sSup_le Ordinal.instNoMaxOrder Set.union_singleton le_trans Monotone.imp OrderHom.monotone le_lfpApprox OrderHom.monotone' lfpApprox_monotone le_sSup Set.mem_union le_refl
lfpApprox_eq_of_mem_fixedPoints 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike Ordinal Ordinal.partialOrder Set Set.instMembership Function.fixedPoints lfpApprox	lfpApprox	—	WellFoundedLT.induction Ordinal.wellFoundedLT le_antisymm lfpApprox.eq_1 sSup_le Set.union_singleton le_lfpApprox lfpApprox_add_one lfpApprox_monotone Ordinal.instNoMaxOrder Function.mem_fixedPoints_iff le_refl
lfpApprox_le_of_mem_fixedPoints 📖	mathematical	Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike Preorder.toLE	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder lfpApprox	—	WellFoundedLT.induction Ordinal.wellFoundedLT lfpApprox.eq_1 sSup_le OrderHom.monotone'
lfpApprox_mem_fixedPoints_of_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike Ordinal Preorder.toLT Ordinal.partialOrder lfpApprox	Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike lfpApprox	—	Function.mem_fixedPoints_iff lfpApprox_add_one Monotone.eq_of_ge_of_le lfpApprox_monotone SuccOrder.le_succ SuccOrder.succ_le_of_lt lfpApprox_eq_of_mem_fixedPoints
lfpApprox_mono_left 📖	mathematical	—	Monotone OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder Pi.preorder Ordinal lfpApprox	—	WellFoundedLT.induction Ordinal.wellFoundedLT lfpApprox.eq_1 sSup_le Set.union_singleton sSup_insert le_sup_of_le_right le_sSup_of_le le_trans OrderHom.monotone
lfpApprox_mono_mid 📖	mathematical	—	Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder Pi.preorder Ordinal lfpApprox	—	WellFoundedLT.induction Ordinal.wellFoundedLT lfpApprox.eq_1 sSup_le Set.union_singleton sSup_insert le_sup_of_le_left le_sup_of_le_right le_sSup_of_le OrderHom.monotone
lfpApprox_monotone 📖	mathematical	—	Monotone Ordinal PartialOrder.toPreorder Ordinal.partialOrder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder lfpApprox	—	lfpApprox.eq_1 sSup_le_sSup Set.union_subset_union lt_of_lt_of_le subset_refl Set.instReflSubset
lfpApprox_ord_eq_lfp 📖	mathematical	—	lfpApprox Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Cardinal.ord Order.succ Cardinal Cardinal.partialOrder Cardinal.instSuccOrder DFunLike.coe OrderHom OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.lfp	—	le_antisymm lfpApprox_le_of_mem_fixedPoints bot_le lfpApprox_ord_mem_fixedPoint OrderHom.lfp_le_fixed Subtype.prop
lfpApprox_ord_mem_fixedPoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom OrderHom.instFunLike	Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instFunLike lfpApprox Cardinal.ord Order.succ Cardinal Cardinal.partialOrder Cardinal.instSuccOrder	—	exists_lfpApprox_eq_lfpApprox le_total lfpApprox_mem_fixedPoints_of_eq Ne.lt_of_le le_of_lt
lfp_mem_range_lfpApprox 📖	mathematical	—	Set Set.instMembership Set.range Ordinal lfpApprox Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder DFunLike.coe OrderHom OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.lfp	—	lfpApprox_ord_eq_lfp

---

← Back to Index