disjoint_image_inl_range_inr — Mathlib

English

Same as previous: disjointness between the left-range and right-image for any v.

Русский

Та же самая формулировка: несовпадение между range Sum.inl и image Sum.inr над v.

LaTeX

$$$\operatorname{Disjoint}(\operatorname{range}(\mathrm{Sum.inl}), \operatorname{image}(\mathrm{Sum.inr}, v))$$$

Lean4

@[simp]
theorem disjoint_image_inl_range_inr {u : Set α} : Disjoint (α := Set (α ⊕ β)) (Sum.inl '' u) (range Sum.inr) :=
  by
  rw [← image_univ]
  apply disjoint_image_inl_image_inr

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