disjoint_map_compl — Mathlib

English

If s is intersecting, then s is disjoint from its image under complementation mapped by an embedding that flips elements.

Русский

Если s пересекается, то оно взаимоисключаемо с образом через отображение комплементов.

LaTeX

$$$\text{Intersecting}(s) \Rightarrow \mathrm{Disjoint}\, s\; (\mathrm{map}\; \langle \complement, \text{compl_injective} \rangle\; s)$$$

Lean4

theorem disjoint_map_compl {s : Finset α} (hs : (s : Set α).Intersecting) :
    Disjoint s (s.map ⟨compl, compl_injective⟩) :=
  by
  rw [Finset.disjoint_left]
  rintro x hx hxc
  obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc
  exact hs.compl_notMem hx' hx

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