Theorems · Definition
iInf
{α : Type u} → {ι : Sort v} → [InfSet α] → (ι → α) → αIndexed infimum
- Defined in
- Mathlib.Order.SetNotation
- Cited by
- 1,690 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 8 definitions · uses no axioms
- Assumes
- InfSet
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.rangeproof · cited by 4,705
- InfSet.sInfproof · cited by 935
- InfSetstatement and proof · cited by 145
Cited by1,811
Results whose statement or proof uses this declaration.
- Filter.atTopproof · cited by 2,405
- Set.iInterproof · cited by 1,084
- Filter.atBotproof · cited by 512
- Cardinal.ordproof · cited by 266
- iInf_congr_Propstatement and proof · cited by 218
- Metric.infEDistproof · cited by 147
- Filter.cocompactproof · cited by 141
- iInf_lestatement · cited by 104
- le_iInfstatement · cited by 102
- LieModule.genWeightSpaceproof · cited by 99
- Order.cofproof · cited by 86
- Ideal.heightproof · cited by 83
Showing the 200 most cited of 1,811.