Mathlib Map

Theorems · Inductive type · order theory

ConditionallyCompletePartialOrderInf

Type u_3 → Type u_3

Conditionally complete partial orders (with infima) are partial orders where every nonempty, directed set which is bounded below has a greatest lower bound.

Defined in
Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Cited by
51 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ciInf_const · cited by 20ciInf_constIsLeast.csInf_eq · cited by 11IsLeast.csInf_eqciInf_unique · cited by 9ciInf_uniqueDirectedOn.csInf_le · cited by 9DirectedOn.csInf_letendsto_atTop_ciInf · cited by 8tendsto_atTop_ciInfDirectedOn.isGLB_csInf · cited by 8DirectedOn.isGLB_csInfcsInf_singleton · cited by 6csInf_singletoncsInf_Ici · cited by 5csInf_IciciInf_pos · cited by 4ciInf_posDirectedOn.le_csInf · cited by 4DirectedOn.le_csInfDirected.ciInf_le · cited by 3Directed.ciInf_lecsInf_Icc · cited by 2csInf_IccDirected.le_ciInf_iff · cited by 2Directed.le_ciInf_iffGaloisConnection.u_ciInf_of_directed · cited by 2GaloisConnection.u_ciInf_…GaloisConnection.u_csInf_of_directedOn · cited by 2GaloisConnection.u_csInf_…ConditionallyCompletePartialO…CITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by57

Results whose statement or proof uses this declaration.