disjoint_filter_filter' — Mathlib

English

Disjoint (S.filter p) (T.filter q) for predicates p,q; in particular, disjointness follows from p and q separation.

Русский

Непересечение (S.filter p) и (T.filter q) для предикатов p,q; в частности, непересечение следует из раздельности p и q.

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{filter}(p, S), \\operatorname{filter}(q, T))$$$

Lean4

theorem disjoint_filter_filter' (s t : Finset α) {p q : α → Prop} [DecidablePred p] [DecidablePred q]
    (h : Disjoint p q) : Disjoint (s.filter p) (t.filter q) :=
  by
  simp_rw [disjoint_left, mem_filter]
  rintro a ⟨_, hp⟩ ⟨_, hq⟩
  rw [Pi.disjoint_iff] at h
  simpa [hp, hq] using h a

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