Theorems · Theorem · field theory
Real.iSup_nonneg
∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ ⨆ i, f iAs ⨆ i, f i = 0 when the domain of the real-valued function f is empty or unbounded above,
it suffices to show that all values of f are nonnegative to show that 0 ≤ ⨆ i, f i.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Realstatement and proof · cited by 25,697
- iSupstatement · cited by 2,415
- Set.forall_mem_rangeproof · cited by 135
- Real.sSup_nonnegproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- Real.iSup_nonneg_of_nonnegHomClassproof · cited by 9
- Height.mulHeight_eval_leproof · cited by 3
- spectralValue_nonnegproof · cited by 2
- spectralNorm_eq_iSup_of_finiteDimensional_normalproof · cited by 2
- max_norm_root_eq_spectralValueproof · cited by 1
- Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonnegproof · cited by 1