card_filter_le_iff — Mathlib

English

Let S be finite and P a decidable predicate. Then #(S.filter P) ≤ #S, i.e., filtering never increases the cardinality.

Русский

Пусть S конечное, P — допускаемое предикат. Тогда #(S.filter P) ≤ #S, то есть фильтрация не увеличивает кардинал.

LaTeX

$$$\\#(s.filter P) \\le \\#s$$$

Lean4

theorem card_filter_le_iff (s : Finset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
    #(s.filter P) ≤ n ↔ ∀ s' ⊆ s, n < #s' → ∃ a ∈ s', ¬P a :=
  (s.1.card_filter_le_iff P n).trans
    ⟨fun H s' hs' h ↦ H s'.1 (by simp_all) h, fun H s' hs' h ↦
      H ⟨s', nodup_of_le hs' s.2⟩ (fun _ hx ↦ Multiset.subset_of_le hs' hx) h⟩

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