Theorems · Theorem · order theory
ciSup_eq_of_forall_le_of_forall_lt_exists_gt
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {b : α} [Nonempty ι] {f : ι → α},
(∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = bIntroduction rule to prove that b is the supremum of f: it suffices to check that b
is larger than f i for all i, and that this is not the case of any w<b.
See iSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- iSupstatement · cited by 2,415
- ConditionallyCompleteLatticestatement and proof · cited by 364
- Set.forall_mem_rangeproof · cited by 135
- Set.range_nonemptyproof · cited by 84
- Set.exists_range_iffproof · cited by 22
- csSup_eq_of_forall_le_of_forall_lt_exists_gtproof · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- rank_subsingletonproof · cited by 19
- PiLp.nnnorm_singleproof · cited by 4
- cbiSup_eq_of_not_forallproof · cited by 2
- IsMaxOn.iSup_eqproof · cited by 2
- lp.norm_singleproof · cited by 1
- spectralValue_X_sub_Cproof · cited by 1
- ciInf_eq_of_forall_ge_of_forall_gt_exists_ltproof · cited by 0
- MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generatedproof · cited by 0