range_comp_val — Mathlib

English

Let S be a subalgebra of A and f: A → B an algebra hom. The range of the restricted map f.subalgebraMap S equals the image S.map f.

Русский

Пусть S — подпалгебра A, и f: A → B алгебра-хом. Образ ограниченного отображения f.subalgebraMap равен S.map f.

LaTeX

$$$\mathrm{range}(f \circ S.{\mathrm{val}}) = S.map f$$$

Lean4

theorem range_comp_val : (f.comp S.val).range = S.map f := by rw [AlgHom.range_comp, range_val]

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