mrange_inl' — Mathlib

English

The range of the left-inclusion equals the preimage of the bottom submonoid under the second projection; i.e., mrange(inl M N) = comap (snd M N) ⊥.

Русский

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

LaTeX

$$$ \operatorname{mrange}(\operatorname{inl} M N) = \operatorname{comap}(\operatorname{snd} M N) \bot $$$

Lean4

@[to_additive]
theorem mrange_inl' : mrange (inl M N) = comap (snd M N) ⊥ :=
  mrange_inl.trans (top_prod _)

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