disjoint_filter_filter — Mathlib

English

If two finite sets s and t are disjoint, then their p-filter and q-filter are disjoint as well, i.e., s.filter p and t.filter q have empty intersection provided s and t are disjoint.

Русский

Если две конечные множества s и t не пересекаются, то их соответственно отфильтрованные по p и по q части тоже не пересекаются.

LaTeX

$$Disjoint(s, t) \\Rightarrow Disjoint(s.filter p, t.filter q)$$

Lean4

theorem disjoint_filter_filter {s t : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
    Disjoint s t → Disjoint (s.filter p) (t.filter q) :=
  Disjoint.mono (filter_subset _ _) (filter_subset _ _)

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