frequently_cocardinal — Mathlib

English

For p, the frequent value in cocardinal relates to the inequality c ≤ |{x : p x}|.

Русский

Для p частота в cocardinal связана с неравенством c ≤ |{x : p(x)}|.

LaTeX

$$Frequently(p in cocardinal α hreg) ⇔ c ≤ |{x : p x}|$$

Lean4

theorem frequently_cocardinal {p : α → Prop} : (∃ᶠ x in cocardinal α hreg, p x) ↔ c ≤ #{x | p x} := by
  simp only [Filter.Frequently, eventually_cocardinal, not_not, coe_setOf, not_lt]

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