FixedPoints

📁 Source: Mathlib/Order/FixedPoints.lean

Statistics

Metric	Count
Definitions gfp, lfp, nextFixed, prevFixed, completeLattice, instBoundedOrderElemFixedPointsCoeOrderHom, instSemilatticeInfElemFixedPointsCoeOrderHom, instSemilatticeSupElemFixedPointsCoeOrderHom	8
Theorems gfp_const_inf_le, gfp_gfp, gfp_induction, gfp_le, gfp_le_map, isFixedPt_gfp, isFixedPt_lfp, isGreatest_gfp, isGreatest_gfp_le, isLeast_lfp, isLeast_lfp_le, le_gfp, le_lfp, le_map_sSup_subset_fixedPoints, le_map_sup_fixedPoints, le_nextFixed, le_prevFixed, le_prevFixed_iff, lfp_induction, lfp_le, lfp_le_fixed, lfp_le_gfp, lfp_le_map, lfp_lfp, map_gfp, map_gfp_comp, map_inf_fixedPoints_le, map_le_gfp, map_le_lfp, map_lfp, map_lfp_comp, map_sInf_subset_fixedPoints_le, nextFixed_le, nextFixed_le_iff, prevFixed_le, gfp_eq_sInf_iterate, lfp_eq_sSup_iterate	37
Total	45

OrderHom

Definitions

Name	Category	Theorems
gfp 📖	CompOp	16 math math: OrdinalApprox.gfp_mem_range_gfpApprox, lfp_le_gfp, gfp_const_inf_le, gfp_le_map, gfp_le, OrdinalApprox.gfpApprox_ord_eq_gfp, gfp_gfp, map_gfp, isGreatest_gfp_le, fixedPoints.gfp_eq_sInf_iterate, isGreatest_gfp, gfp_induction, isFixedPt_gfp, le_gfp, map_gfp_comp, map_le_gfp
lfp 📖	CompOp	16 math math: lfp_induction, lfp_le_gfp, map_lfp, isLeast_lfp, OrdinalApprox.lfpApprox_ord_eq_lfp, lfp_lfp, le_lfp, isFixedPt_lfp, map_le_lfp, fixedPoints.lfp_eq_sSup_iterate, OrdinalApprox.lfp_mem_range_lfpApprox, lfp_le, isLeast_lfp_le, map_lfp_comp, lfp_le_map, lfp_le_fixed
nextFixed 📖	CompOp	3 math math: nextFixed_le, nextFixed_le_iff, le_nextFixed
prevFixed 📖	CompOp	3 math math: le_prevFixed, le_prevFixed_iff, prevFixed_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gfp_const_inf_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp instMin Lattice.toSemilatticeInf CompleteLattice.toLattice const	—	gfp_le LE.le.trans inf_le_left
gfp_gfp 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instPreorder instFunLike gfp comp onDiag	—	lfp_lfp
gfp_induction 📖	mathematical	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike InfSet.sInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instPreorder instFunLike gfp	—	lfp_induction
gfp_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp	—	sSup_le
gfp_le_map 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp	—	map_le_lfp
isFixedPt_gfp 📖	mathematical	—	Function.IsFixedPt DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike instPreorder gfp	—	isFixedPt_lfp
isFixedPt_lfp 📖	mathematical	—	Function.IsFixedPt DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike instPreorder lfp	—	map_lfp
isGreatest_gfp 📖	mathematical	—	IsGreatest Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder Function.fixedPoints DFunLike.coe OrderHom instFunLike instPreorder gfp	—	isLeast_lfp
isGreatest_gfp_le 📖	mathematical	—	IsGreatest Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder setOf DFunLike.coe OrderHom instFunLike instPreorder gfp	—	isLeast_lfp_le
isLeast_lfp 📖	mathematical	—	IsLeast Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder Function.fixedPoints DFunLike.coe OrderHom instFunLike instPreorder lfp	—	isFixedPt_lfp lfp_le_fixed
isLeast_lfp_le 📖	mathematical	—	IsLeast Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder setOf DFunLike.coe OrderHom instFunLike instPreorder lfp	—	Eq.le map_lfp lfp_le
le_gfp 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp	—	le_sSup
le_lfp 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp	—	le_sInf
le_map_sSup_subset_fixedPoints 📖	mathematical	Set Set.instHasSubset Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup DFunLike.coe OrderHom instFunLike	—	sSup_le mono le_sSup
le_map_sup_fixedPoints 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom instFunLike	—	Monotone.le_map_sup mono
le_nextFixed 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom instFunLike nextFixed	—	prevFixed_le
le_prevFixed 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike Set Set.instMembership Function.fixedPoints	Set.Elem Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike Preorder.toLE Set Set.instMembership prevFixed	—	le_prevFixed_iff
le_prevFixed_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Set.Elem Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike Preorder.toLE Set Set.instMembership prevFixed	—	nextFixed_le_iff
lfp_induction 📖	mathematical	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instPreorder instFunLike lfp	—	sSup_le map_le_lfp LE.le.antisymm lfp_le le_sSup
lfp_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp	—	sInf_le
lfp_le_fixed 📖	mathematical	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp	—	lfp_le Eq.le
lfp_le_gfp 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp gfp	—	lfp_le_fixed isFixedPt_gfp
lfp_le_map 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp	—	map_lfp mono
lfp_lfp 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instPreorder instFunLike lfp comp onDiag	—	LE.le.antisymm lfp_le Eq.le map_lfp
map_gfp 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike instPreorder gfp	—	map_lfp
map_gfp_comp 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike instPreorder gfp comp	—	map_lfp_comp
map_inf_fixedPoints_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice Set Set.instMembership Function.fixedPoints	—	le_map_sup_fixedPoints
map_le_gfp 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike instPreorder gfp	—	lfp_le_map
map_le_lfp 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike lfp	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike instPreorder lfp	—	le_lfp LE.le.trans mono le_sInf_iff
map_lfp 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike instPreorder lfp	—	map_le_lfp le_rfl LE.le.antisymm lfp_le mono
map_lfp_comp 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike instPreorder lfp comp	—	le_antisymm mono lfp_le_fixed map_lfp lfp_le Eq.le
map_sInf_subset_fixedPoints_le 📖	mathematical	Set Set.instHasSubset Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike InfSet.sInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf	—	le_sInf mono sInf_le
nextFixed_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike Set Set.instMembership Function.fixedPoints	Set.Elem Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike Preorder.toLE Set Set.instMembership nextFixed	—	Subtype.coe_le_coe lfp_le sup_le Eq.le
nextFixed_le_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Set.Elem Function.fixedPoints DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike Preorder.toLE Set Set.instMembership nextFixed	—	LE.le.trans le_nextFixed nextFixed_le
prevFixed_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder Set Set.instMembership Function.fixedPoints DFunLike.coe OrderHom instFunLike prevFixed	—	gfp_const_inf_le

fixedPoints

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	—
instBoundedOrderElemFixedPointsCoeOrderHom 📖	CompOp	—
instSemilatticeInfElemFixedPointsCoeOrderHom 📖	CompOp	—
instSemilatticeSupElemFixedPointsCoeOrderHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gfp_eq_sInf_iterate 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous OrderDual CompleteLattice.instOmegaCompletePartialOrder OrderDual.instCompleteLattice DFunLike.coe OrderHom OrderDual.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike OrderHom.dual	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.gfp iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Nat.iterate Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	lfp_eq_sSup_iterate
lfp_eq_sSup_iterate 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.lfp iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Nat.iterate Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	le_antisymm OrderHom.lfp_le_fixed Function.mem_fixedPoints OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom bot_le OrderHom.le_lfp OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint

---

← Back to Index