Theorems · Theorem · order theory
iInf_le_of_le
∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι), f i ≤ a → iInf f ≤ a- Defined in
- Mathlib.Order.CompleteLattice.Basic
- Cited by
- 62 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- CompleteLattice
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.
- iInfstatement · cited by 1,690
- CompleteLatticestatement and proof · cited by 1,048
- LE.le.trans'proof · cited by 140
- iInf_leproof · cited by 104
Cited by62
Results whose statement or proof uses this declaration.
- iInf₂_leproof · cited by 45
- iInf_monoproof · cited by 29
- Finset.inf_eq_iInfproof · cited by 19
- Filter.mem_lift'proof · cited by 15
- MeasureTheory.OuterMeasure.ofFunction_leproof · cited by 10
- iInf_mono'proof · cited by 10
- Set.iInter_subset_of_subsetproof · cited by 9
- MeasureTheory.inducedOuterMeasure_eq_iInfproof · cited by 7
- LowerSemicontinuousOn.exists_isMinOnproof · cited by 6
- MeasureTheory.Measure.nullSingletonClass_hausdorffproof · cited by 5
- MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trimproof · cited by 4
- Filter.mem_liftproof · cited by 3