range_comp — Mathlib

English

If f is surjective, then range(g ∘ f) = range(g).

Русский

Если f сюръективно, тогда диапазон (g ∘ f) равен диапазону g.

LaTeX

$$$\operatorname{range}(g \circ f) = \operatorname{range}(g) \quad\text{при } \text{Surjective } f.$$$

Lean4

theorem range_comp {ι' : Sort*} {f : ι → ι'} (hf : Surjective f) (g : ι' → α) : range (g ∘ f) = range g :=
  ext fun y => (@Surjective.exists _ _ _ hf fun x => g x = y).symm

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