Mathlib Map

Theorems · Theorem · order theory

sup_le_inf

∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊔ b ≤ a ⊓ b ↔ a = b
Defined in
Mathlib.Order.Lattice
Cited by
2 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext
Assumes
Lattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

inf_eq_sup · cited by 2inf_eq_supsup_eq_inf · cited by 1sup_eq_infLattice · cited by 916Latticesup_le_infCITED BYCITES

Cites1

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

  • Latticestatement and proof · cited by 916

Cited by2

Results whose statement or proof uses this declaration.