essSup_smul_measure — Mathlib

English

Nonzero scalar c does not change essSup when acting on measure, under appropriate scalar-tower hypotheses.

Русский

Ненулевой скаляр не изменяет essSup при действии на меру (при некоторых тензорных условностях).

LaTeX

$$$hc \neq 0 \Rightarrow \operatorname{essSup} f (c \cdot μ) = \operatorname{essSup} f μ$.$$

Lean4

@[simp]
theorem essSup_smul_measure (hc : c ≠ 0) (f : α → β) : essSup f (c • μ) = essSup f μ := by
  simp_rw [essSup, Measure.ae_smul_measure_eq hc]

Похожие утверждения