of_map — Mathlib

English

If f and g are simple functions with finite μ-measurable support, then their pair has finite μ-measurable support.

Русский

Если f и g — простые функции с конечной μ-опорой, то их пара имеет конечную μ-опору.

LaTeX

$$$\mathrm{FinMeasSupp}(f,\mu) \to \mathrm{FinMeasSupp}(g,\mu) \to \mathrm{FinMeasSupp}(\mathrm{pair}(f,g),\mu)$$$

Lean4

theorem of_map {g : β → γ} (h : (f.map g).FinMeasSupp μ) (hg : ∀ b, g b = 0 → b = 0) : f.FinMeasSupp μ :=
  flip lt_of_le_of_lt h <| measure_mono <| support_subset_comp @(hg) _

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