card_subtype_lt — Mathlib

English

For finite α and predicate p and x with ¬p(x), Nat.card { x ∈ α : p x } < Nat.card α.

Русский

Для конечного α и p и x с ¬p(x), Nat.card { x ∈ α : p(x) } < Nat.card α.

LaTeX

$$$Nat.card(\{ x \mid p(x) \}) < Nat.card(\alpha)$$$

Lean4

theorem card_subtype_lt [Finite α] {p : α → Prop} {x : α} (hx : ¬p x) : Nat.card { x // p x } < Nat.card α := by
  classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

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