Theorems · Theorem · order theory
sInf_eq_iInf
∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⨅ a ∈ s, a- Defined in
- Mathlib.Order.CompleteLattice.Basic
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- iInfstatement · cited by 1,690
- CompleteLatticestatement and proof · cited by 1,048
- InfSet.sInfstatement · cited by 935
- sInf_leproof · cited by 110
- le_iInf₂proof · cited by 67
- le_sInfproof · cited by 51
- ge_antisymmproof · cited by 51
- iInf₂_leproof · cited by 45
Cited by22
Results whose statement or proof uses this declaration.
- GaloisConnection.u_sInfproof · cited by 11
- Monotone.map_sInf_leproof · cited by 4
- Finset.inf_id_eq_sInfproof · cited by 4
- OrderIso.map_sInfproof · cited by 3
- Ideal.comap_jacobsonproof · cited by 2
- Ideal.comap_jacobson_of_surjectiveproof · cited by 2
- sInf_sup_sInfproof · cited by 1
- Ideal.IsHomogeneous.sInfproof · cited by 1
- MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrictproof · cited by 1
- isJacobsonRing_localizationproof · cited by 1
- compl_sInfproof · cited by 1
- PointedCone.ofSubmodule_iInfproof · cited by 0