Theorems · Definition
InfSet.sInf
{α : Type u_1} → [self : InfSet α] → Set α → αInfimum of a set
- Defined in
- Mathlib.Order.SetNotation
- Cited by
- 935 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- InfSet
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by1,081
Results whose statement or proof uses this declaration.
- iInfproof · cited by 1,690
- Submodule.spanproof · cited by 1,504
- Set.sInterproof · cited by 225
- AddSubmonoid.closureproof · cited by 224
- Subgroup.closureproof · cited by 196
- Submonoid.closureproof · cited by 167
- AddSubgroup.closureproof · cited by 156
- sInf_lestatement · cited by 110
- Ideal.jacobsonproof · cited by 88
- gaugeproof · cited by 85
- Subring.closureproof · cited by 78
- FirstOrder.Language.Substructure.closureproof · cited by 70
Showing the 200 most cited of 1,081.