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	14 math math: OrdinalApprox.gfp_mem_range_gfpApprox, lfp_le_gfp, gfp_const_inf_le, 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
lfp 📖	CompOp	14 math math: lfp_induction, lfp_le_gfp, map_lfp, isLeast_lfp, OrdinalApprox.lfpApprox_ord_eq_lfp, lfp_lfp, le_lfp, isFixedPt_lfp, fixedPoints.lfp_eq_sSup_iterate, OrdinalApprox.lfp_mem_range_lfpApprox, lfp_le, isLeast_lfp_le, map_lfp_comp, 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	instPreorder gfp	—	lfp_induction
gfp_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder	DFunLike.coe OrderHom instPreorder instFunLike gfp	—	sSup_le
gfp_le_map 📖	—	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	instPreorder gfp	—	le_sSup
le_lfp 📖	mathematical	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 SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	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	Set Set.instMembership Function.fixedPoints 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 prevFixed	—	le_prevFixed_iff
le_prevFixed_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instFunLike	Set.Elem Function.fixedPoints 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	instPreorder 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	instPreorder lfp	—	sInf_le
lfp_le_fixed 📖	mathematical	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLike	Preorder.toLE instPreorder 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 📖	—	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 📖	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike gfp	—	—	lfp_le_map
map_le_lfp 📖	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder DFunLike.coe OrderHom instPreorder instFunLike 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 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 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 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	Set Set.instMembership Function.fixedPoints 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	OrderHom.instPreorder 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	OrderHom.instPreorder 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