Theorems · Theorem · order theory
inf_le_sup
∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ b ≤ a ⊔ b- Defined in
- Mathlib.Order.Lattice
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Lattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LE.le.transproof · cited by 3,151
- Latticestatement and proof · cited by 916
- inf_le_leftproof · cited by 286
- le_sup_leftproof · cited by 265
Cited by14
Results whose statement or proof uses this declaration.
- Finset.inter_subset_unionproof · cited by 9
- MeromorphicOn.intervalIntegrable_log_normproof · cited by 4
- symmDiff_sup_infproof · cited by 2
- Set.nonempty_uIccproof · cited by 2
- inf_eq_supproof · cited by 2
- bihimp_inf_supproof · cited by 2
- inf_lt_supproof · cited by 2
- Finset.uIcc_subset_uIcc_iff_le'proof · cited by 1
- Set.uIcc_subset_uIcc_iff_le'proof · cited by 1
- Equiv.Perm.prod_Iio_comp_eq_sign_mul_prodproof · cited by 1
- sup_eq_infproof · cited by 1
- sup_sdiff_symmDiffproof · cited by 1