Mathlib Map

Theorems · Theorem · order theory

OrderHom.lfp_le

∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, f a ≤ a → OrderHom.lfp f ≤ a
Defined in
Mathlib.Order.FixedPoints
Cited by
7 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext
Assumes
CompleteLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

OrderHom.map_lfp · cited by 7OrderHom.map_lfpOrderHom.lfp_le_fixed · cited by 5OrderHom.lfp_le_fixedOrderHom.nextFixed_le · cited by 2OrderHom.nextFixed_leOrderHom.isLeast_lfp_le · cited by 1OrderHom.isLeast_lfp_leOrderHom.lfp_lfp · cited by 1OrderHom.lfp_lfpOrderHom.map_lfp_comp · cited by 1OrderHom.map_lfp_compOrderHom.lfp_induction · cited by 1OrderHom.lfp_inductionDFunLike.coe · cited by 62936DFunLike.coeCompleteLattice · cited by 1048CompleteLatticeOrderHom · cited by 934OrderHomsInf_le · cited by 110sInf_leOrderHom.lfp · cited by 17OrderHom.lfpOrderHom.lfp_leCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by7

Results whose statement or proof uses this declaration.