disjoint_map_inl_map_inr — Mathlib

English

If we map elements of s into the left component and elements of t into the right component, the resulting Finsets are disjoint: map_inl(s) and map_inr(t) have empty intersection.

Русский

Если отображать элементы s в левую компоненту и элементы t в правую компоненту, полученные множества не пересекаются: изображения inl(s) и inr(t) разрезаются в пустое множество.

LaTeX

$$$\mathrm{Disjoint}(s^{\mathrm{inl}}, t^{\mathrm{inr}})$$$

Lean4

theorem disjoint_map_inl_map_inr : Disjoint (s.map Embedding.inl) (t.map Embedding.inr) :=
  by
  simp_rw [disjoint_left, mem_map]
  rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩

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