disjoint_filter_and_not_filter — Mathlib

English

The two filtered subfamilies of a Finset s, namely those with p ∧ ¬q and those with q ∧ ¬p, are disjoint.

Русский

Подмножества Finset, состоящие из элементов, удовлетворяющих p и не q, и из элементов, удовлетворяющих q и не p, не пересекаются.

LaTeX

$$Disjoint( s.filter(\\lambda x, p x ∧ ¬ q x), s.filter(\\lambda x, q x ∧ ¬ p x) )$$

Lean4

theorem disjoint_filter_and_not_filter : Disjoint (s.filter (fun x ↦ p x ∧ ¬q x)) (s.filter (fun x ↦ q x ∧ ¬p x)) :=
  by
  intro _ htp htq
  simp only [bot_eq_empty, le_eq_subset, subset_empty, ← not_nonempty_iff_eq_empty]
  rintro ⟨_, hx⟩
  exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1

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