Theorems · Theorem · order theory
le_iSup_iff
∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteSemilatticeSup α] {a : α} {s : ι → α},
a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, Quot.sound
- Assumes
- CompleteSemilatticeSup
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.ofPredproof · cited by 6,101
- iSupstatement · cited by 2,415
- CompleteSemilatticeSupstatement and proof · cited by 18
Cited by16
Results whose statement or proof uses this declaration.
- Set.encard_le_chainHeight_of_isChainproof · cited by 6
- ENat.mul_iSupproof · cited by 3
- HahnEmbedding.Seed.mem_domain_baseEmbeddingproof · cited by 2
- Order.krullDim_eq_topproof · cited by 2
- MeasureTheory.OuterMeasure.mkMetric_topproof · cited by 1
- FirstOrder.Language.DirectLimit.cgproof · cited by 1
- LTSeries.height_last_longestOfproof · cited by 1
- CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSupproof · cited by 1
- tendsto_iSup_of_tendsto_limsupproof · cited by 1
- PSL.iSup_lineStab_eq_topproof · cited by 1
- Order.krullDim_le_of_krullDim_preimage_leproof · cited by 1
- AddSubmonoid.mem_iSupproof · cited by 0