mrange_inl_sup_mrange_inr — Mathlib

English

The join of the ranges of inl and inr equals the top submonoid of M × N.

Русский

Слияние образов inl и inr равно верхнему подмонойду M × N.

LaTeX

$$$ \operatorname{mrange}(\operatorname{inl} M N) \sqcup \operatorname{mrange}(\operatorname{inr} M N) = \top $$$

Lean4

@[to_additive (attr := simp)]
theorem mrange_inl_sup_mrange_inr : mrange (inl M N) ⊔ mrange (inr M N) = ⊤ := by
  simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]

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