productMap_range — Mathlib

English

The range of the product map is the supremum of the ranges of f and g.

Русский

Образ productMap равен наименьшему верхнему предельному элементу над образами f и g.

LaTeX

$$(productMap f g).range = f.range ⊔ g.range$$

Lean4

theorem productMap_range : (productMap f g).range = f.range ⊔ g.range := by
  rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp, ← AlgHom.range_comp, ←
    AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight, AlgHom.id_comp,
    AlgHom.id_comp]

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