coe_range — Mathlib

English

The range of the composition g ∘ f equals the image under g of the range of f: range(g ∘ f) = range(f).map g.

Русский

Образ композиции g ∘ f равен образу f под действием g: range(g ∘ f) = range(f).map g.

LaTeX

$$$\\mathrm{range}(g\\circ f) = \\mathrm{range}(f).map\\,g$$$

Lean4

@[simp]
theorem coe_range (φ : F) : ((NonUnitalAlgHom.range φ : NonUnitalSubalgebra R B) : Set B) = Set.range (φ : A → B) :=
  by
  ext
  rw [SetLike.mem_coe, mem_range, Set.mem_range]

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