English
Let s be a finite multiset of elements of α and P a decidable predicate on α. For any natural number n, the inequality card(s.filter P) ≤ n holds exactly when every submultiset s′ of s with more than n elements contains an element outside P (i.e., not in P).
Русский
Пусть s — конечный мультисет элементов α, P — определимый предикат на α. Для любого n ∈ ℕ неравенство card(s.filter P) ≤ n выполняется тогда и только тогда, когда каждый подпульс (подмножество) s′ ≤ s с cardinality > n содержит элемент, не удовлетворяющий P.
LaTeX
$$$\operatorname{card}(s\text{.filter } P) \le n \iff \forall s' \le s,\ n < \operatorname{card} s' \to \exists a \in s', \lnot P a$$$
Lean4
theorem card_filter_le_iff (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
card (s.filter P) ≤ n ↔ ∀ s' ≤ s, n < card s' → ∃ a ∈ s', ¬P a :=
by
fconstructor
· intro H s' hs' s'_card
by_contra! rid
have card := card_le_card (monotone_filter_left P hs') |>.trans H
exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)
· contrapose!
exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩
