mrange_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mrange_inl : mrange (inl M N) = prod ⊤ ⊥ := by simpa only [mrange_eq_map] using map_inl ⊤

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