range_lift — Mathlib

English

The range of the lift map from two homomorphisms f: G →* K and g: H →* K equals the supremum of the two ranges.

Русский

Образ отображения lift от двух гомоморфизмов f и g равен верхней границе двух образов.

LaTeX

$$$\mathrm{range}(\mathrm{lift}\; f\; g) = \mathrm{range}(f) \sqcup \mathrm{range}(g).$$$

Lean4

@[to_additive (attr := simp)]
theorem range_lift (f : G →* K) (g : H →* K) : MonoidHom.range (lift f g) = MonoidHom.range f ⊔ MonoidHom.range g := by
  simp [range_eq]

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