Theorems · Theorem · real analysis
ENNReal.smul_sSup
∀ {R : Type u_3} [inst : SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (s : Set ENNReal) (c : R),
c • sSup s = ⨆ a ∈ s, c • a- Defined in
- Mathlib.Data.ENNReal.Inv
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SMulIsScalarTower
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- ENNRealstatement and proof · cited by 9,879
- IsScalarTowerstatement and proof · cited by 3,896
- iSupstatement and proof · cited by 2,415
- SupSet.sSupstatement and proof · cited by 954
- iSup_congr_Propproof · cited by 247
- smul_one_mulproof · cited by 15
- ENNReal.mul_sSupproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.