cardinalInterFilter_aleph0 — Mathlib

English

Every filter is a CardinalInterFilter with c = ℵ₀.

Русский

Каждый фильтр является CardinalInterFilter с параметром c = ℵ₀.

LaTeX

$$$$ \\text{Filter } l \\Rightarrow \\text{CardinalInterFilter } l \\aleph_0 $$$$

Lean4

/-- Every filter is a CardinalInterFilter with c = ℵ₀ -/
theorem _root_.Filter.cardinalInterFilter_aleph0 (l : Filter α) : CardinalInterFilter l ℵ₀ where
  cardinal_sInter_mem := by simp_all only [lt_aleph0_iff_subtype_finite, setOf_mem_eq, sInter_mem, implies_true]

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