frequently_cocardinal_mem — Mathlib

English

A set is frequently true in cocardinal iff the cardinality of the predicate set is at least c.

Русский

Множество часто истинно в cocardinal тогда, когда кардинальность множества элементов, удовлетворяющих условию, не меньше c.

LaTeX

$$frequently_cocardinal_mem {s : Set α} : (∃ᶠ x in cocardinal α hreg, x ∈ s) ↔ c ≤ #s$$

Lean4

theorem frequently_cocardinal_mem {s : Set α} : (∃ᶠ x in cocardinal α hreg, x ∈ s) ↔ c ≤ #s :=
  frequently_cocardinal

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