pairwiseDisjoint_pair_insert — Mathlib

English

If a ∉ s, then the family { {t, t ∪ {a}} : t ∈ s } (viewed as elements of the power set of α) is pairwise disjoint.

Русский

Если a ∉ s, то семейство { {t, t ∪ {a}} : t ∈ s } (как элементы множества подмножеств α) попарно непересекается.

LaTeX

$$$\\displaystyle \\forall t_1,t_2\\in s\\; (t_1 \\neq t_2) \\Rightarrow \\bigl\\{t_1, t_1 \\cup \\{a\\}\\bigr\\} \\cap \\bigl\\{t_2, t_2 \\cup \\{a\\}\\bigr\\} = \\emptyset$$$

Lean4

theorem pairwiseDisjoint_pair_insert {s : Set α} {a : α} (ha : a ∉ s) :
    s.powerset.PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Set α)) :=
  by
  rw [pairwiseDisjoint_iff]
  rintro i hi j hj
  have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)
  aesop (add simp [Set.Nonempty, Set.subset_def])

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