English
If a ∉ s, then the family of two-element sets {t, t ∪ {a}} for t ⊆ s is pairwise disjoint when viewed as sets of subsets.
Русский
Пусть a не принадлежит s. Тогда семейство двойственных множеств {t, t ∪ {a}} для t ⊆ s consists of pairwise disjoint sets.
LaTeX
$$For all t1 ≠ t2 with t1,t2 ⊆ s, {t1, t1 ∪ {a}} ∩ {t2, t2 ∪ {a}} = ∅, provided a ∉ s.$$
Lean4
theorem pairwiseDisjoint_pair_insert [DecidableEq α] {a : α} (ha : a ∉ s) :
(s.powerset : Set (Finset α)).PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Finset α)) :=
by
simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]
rintro i hi j hj
simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff, exists_eq_or_imp,
exists_eq_left, or_imp, imp_self, true_and]
refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩ <;> rintro rfl <;>
cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)
