eventually_cocardinal — Mathlib

English

For any predicate p, the statement 'p holds eventually in cocardinal' is equivalent to the cardinality condition on the set where p fails.

Русский

Для произвольного p утверждение о том, что p выполняется почти всюду в cocardinal, эквивалентно условию по кардинальности множества, где p ложно.

LaTeX

$$$\forall p, (\forallᶠ x \in cocardinal(α,hreg), p(x)) \iff |\{x : p(x)^{c}\}| < c$$$

Lean4

@[simp]
theorem eventually_cocardinal {p : α → Prop} : (∀ᶠ x in cocardinal α hreg, p x) ↔ #{x | ¬p x} < c :=
  Iff.rfl

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