Theorems · Theorem · field theory
Real.iSup_of_isEmpty
∀ {ι : Sort u_1} [IsEmpty ι] (f : ι → ℝ), ⨆ i, f i = 0- Cited by
- 14 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- IsEmpty
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.rangeproof · cited by 4,705
- iSupstatement · cited by 2,415
- SupSet.sSupproof · cited by 954
- IsEmptystatement and proof · cited by 759
- SupSetproof · cited by 154
- Real.sSup_emptyproof · cited by 17
- Set.range_eq_empty_iffproof · cited by 5
Cited by14
Results whose statement or proof uses this declaration.
- lp.norm_nonneg'proof · cited by 6
- Real.iSup_const_zeroproof · cited by 3
- Height.max_mulHeightBound_zero_one_eq_oneproof · cited by 2
- ConvexOn.sSup_of_nat_affine_eqproof · cited by 2
- IsNonarchimedean.apply_sum_leproof · cited by 2
- IsUltrametricDist.norm_tprod_leproof · cited by 2
- IsUltrametricDist.norm_tsum_leproof · cited by 2
- Real.iSup_prod_eq_prod_iSup_of_nonnegproof · cited by 1
- IsNonarchimedean.eval_mvPolynomial_leproof · cited by 1
- IsNonarchimedean.iSup_abv_linearMap_apply_leproof · cited by 1
- OrthonormalBasis.norm_le_card_mul_iSup_norm_innerproof · cited by 1
- Seminorm.sSup_emptyproof · cited by 1