dens_filter_add_dens_filter_not_eq_dens

English

Not disjoint iff there exists an element belonging to both sets.

Русский

Не пересекаются тогда и только тогда, когда существует элемент, принадлежащий обоим множествам.

LaTeX

$$$ \\lnot \\operatorname{Disjoint}(s,t) \\iff \\exists a, a \\in s \\land a \\in t $$$

Lean4

theorem dens_filter_add_dens_filter_not_eq_dens {α : Type*} [Fintype α] {s : Finset α} (p : α → Prop) [DecidablePred p]
    [∀ x, Decidable (¬p x)] : dens ({a ∈ s | p a}) + dens ({a ∈ s | ¬p a}) = dens s := by
  classical rw [← dens_union_of_disjoint (disjoint_filter_filter_neg ..), filter_union_filter_neg_eq]

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