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	10 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`
`lfpApprox` 📖	CompOp	10 math math: `lfpApprox_mono_mid`, `lfpApprox_ord_eq_lfp`, `lfpApprox_le_of_mem_fixedPoints`, `lfpApprox_ord_mem_fixedPoint`, `lfpApprox_monotone`, `lfpApprox_add_one`, `lfpApprox_mono_left`, `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`	—	`lfpApprox_add_one`
`gfpApprox_antitone` 📖	mathematical	—	`Antitone` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `gfpApprox`	—	`lfpApprox_monotone`
`gfpApprox_eq_of_mem_fixedPoints` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `Ordinal` `Ordinal.partialOrder` `Set` `Set.instMembership` `Function.fixedPoints` `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` `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`	`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`	—	`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` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `Ordinal` `Ordinal.partialOrder` `Set` `Set.instMembership` `Function.fixedPoints` `lfpApprox`	—	—	`Ordinal.induction` `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`	`lfpApprox`	—	`Ordinal.induction` `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`	—	`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`	—	`Ordinal.induction` `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`	—	`Ordinal.induction` `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` `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