countP_eq_card — Mathlib

English

countP p s equals the card of s iff every a in s satisfies p a.

Русский

countP p s равно кардинальности s тогда и только тогда, когда для каждого a ∈ s выполняется p a.

LaTeX

$$$\operatorname{countP}(p, s) = \operatorname{card}(s) \iff \forall a \in s, p(a)$$$

Lean4

theorem countP_eq_card {s} : countP p s = card s ↔ ∀ a ∈ s, p a :=
  Quot.inductionOn s fun _l => by simp [List.countP_eq_length]

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