codisjoint_range_inl_range_inr — Mathlib

English

The ranges of inl and inr are codisjoint: they intersect only in the identity element when interpreted in the coproduct.

Русский

Образы inl и inr кодиссоинты: их пересечение в копродукте содержит только единицу.

LaTeX

$$$\text{Codisjoint}(\mathrm{range}(\mathrm{inl}), \mathrm{range}(\mathrm{inr})).$$$

Lean4

@[to_additive]
theorem codisjoint_range_inl_range_inr : Codisjoint (MonoidHom.range (inl : G →* G ∗ H)) (MonoidHom.range inr) :=
  codisjoint_iff.2 range_inl_sup_range_inr

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