disjoint_range_inl_image_inr — Mathlib

English

Disjoint between the entire left-injection range and the image of the right-injection over a set v.

Русский

Не пересекаются множество всех элементов, полученных через Sum.inl, и образ Sum.inr над v.

LaTeX

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

Lean4

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

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