mrange_inr — Mathlib

English

Let inr M N be the right-inclusion monoid hom from M to M × N sending n to (1, n). Its range is the submonoid of all pairs (1, n).

Русский

Пусть inr M N — правое включение M в M × N, откуда n ↦ (1, n). Его образ — подмоноид всех пар (1, n).

LaTeX

$$$ \operatorname{mrange}(\operatorname{inr} M N) = \mathrm{prod} \bot \top $$$

Lean4

@[to_additive]
theorem mrange_inr : mrange (inr M N) = prod ⊥ ⊤ := by simpa only [mrange_eq_map] using map_inr ⊤

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