mrange_lift — Mathlib

English

For monoid homomorphisms f:M →* P and g:N →* P, the monoid-range of lift f g equals the join (supremum) of the ranges of f and g: mrange(lift f g) = mrange f ⊔ mrange g.

Русский

Для моноид-гомоморфизмов f:M →* P и g:N →* P множество значений (образ) lift f g равно объединению (верхнему пределу) образов f и g: mrange(lift f g) = mrange f ⊔ mrange g.

LaTeX

$$$\\\\operatorname{mrange}(\\\\mathrm{lift}\\\\ f\\\\ g) = \\\\operatorname{mrange}(f) \\\\sqcup \\\\operatorname{mrange}(g).$$$

Lean4

@[to_additive (attr := simp)]
theorem mrange_lift (f : M →* P) (g : N →* P) : MonoidHom.mrange (lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g :=
  by simp [mrange_eq]

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