Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.smul_apply

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
  [inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal]
  (c : R) (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω), (c • μ) s = c • μ s

Defined in: Mathlib.MeasureTheory.Measure.FiniteMeasure
Cited by: 1 results in Mathlib
Foundations: Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace SMul SMul IsScalarTower IsScalarTower IsScalarTower

Mathlib docs Source Loogle LeanSearch

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.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
ENNRealstatement and proof · cited by 9,879
NNRealstatement and proof · cited by 4,310
IsScalarTowerstatement and proof · cited by 3,896
MeasureTheory.FiniteMeasurestatement and proof · cited by 150
Pi.smul_applyproof · cited by 28
MeasureTheory.FiniteMeasure.coeFn_smulproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalizeproof · cited by 2