disjoint_filter — Mathlib

English

Disjoint (S.filter p) (S.filter q) iff ∀ x ∈ S, p(x) → ¬ q(x).

Русский

Непересечение (S фильтр) по p и (S фильтр) по q эквивалентно ∀ x ∈ S, p(x) → ¬q(x).

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{filter}(p, S), \\operatorname{filter}(q, S)) \\iff \\forall x \\in S,\\ p(x) \\rightarrow \\neg q(x)$$$

Lean4

theorem disjoint_filter {s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
    Disjoint (s.filter p) (s.filter q) ↔ ∀ x ∈ s, p x → ¬q x := by constructor <;> simp +contextual [disjoint_left]

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