range_comp_subset_range — Mathlib

English

If f is a simple function β → γ and g: α → β is measurable, then the range of f ∘ g is contained in the range of f.

Русский

Если f — простая функция β → γ и g: α → β измерима, то диапазон f ∘ g вложен в диапазон f.

LaTeX

$$$$ \\mathrm{range}(f \\circ g) \\subseteq \\mathrm{range}(f). $$$$

Lean4

theorem range_comp_subset_range [MeasurableSpace β] (f : β →ₛ γ) {g : α → β} (hgm : Measurable g) :
    (f.comp g hgm).range ⊆ f.range :=
  Finset.coe_subset.1 <| by simp only [coe_range, coe_comp, Set.range_comp_subset_range]

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