range_inl_inter_range_inr — Mathlib

English

The left and right injections have disjoint images: the intersection of their ranges is empty.

Русский

Образы влево- и вправо-вставок не пересекаются: пересечение образов пусто.

LaTeX

$$$\operatorname{range}(\mathrm{Sum.inl}) \cap \operatorname{range}(\mathrm{Sum.inr}) = \emptyset$$$

Lean4

@[simp]
theorem range_inl_inter_range_inr : range (Sum.inl : α → α ⊕ β) ∩ range Sum.inr = ∅ :=
  isCompl_range_inl_range_inr.inf_eq_bot

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