mrange_inr' — Mathlib

English

The range of the right-inclusion equals the preimage of the bottom submonoid under the first projection; i.e., mrange(inr M N) = comap (fst M N) ⊥.

Русский

Образ right-inclusion равен предобразу нулевого подмонойда под первой проекции: mrange(inr M N) = comap (fst M N) ⊥.

LaTeX

$$$ \operatorname{mrange}(\operatorname{inr} M N) = \operatorname{comap}(\operatorname{fst} M N) \bot $$$

Lean4

@[to_additive]
theorem mrange_inr' : mrange (inr M N) = comap (fst M N) ⊥ :=
  mrange_inr.trans (prod_top _)

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