Theorems · Theorem · order theory
le_sInf
∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, (∀ b ∈ s, a ≤ b) → a ≤ sInf s- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- CompleteSemilatticeInf
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.
- Setstatement and proof · cited by 53,352
- InfSet.sInfstatement · cited by 935
- isGLB_sInfproof · cited by 23
- CompleteSemilatticeInfstatement and proof · cited by 19
Cited by51
Results whose statement or proof uses this declaration.
- le_iInfproof · cited by 102
- sInf_eq_iInfproof · cited by 22
- Ideal.radical_eq_sInfproof · cited by 21
- IsLocalRing.maximalIdeal_le_jacobsonproof · cited by 16
- Set.subset_sInterproof · cited by 8
- MeasureTheory.Measure.sub_applyproof · cited by 5
- sInf_eq_topproof · cited by 5
- Filter.HasBasis.limsSup_eq_iInf_sSupproof · cited by 5
- FirstOrder.Language.Substructure.coe_closure_eq_range_term_realizeproof · cited by 3
- Localization.r_eq_r'proof · cited by 3
- Ideal.map_sInfproof · cited by 3
- ENNReal.coe_inv_leproof · cited by 3