of_cardinalInterFilter_of_lt — Mathlib

English

If a filter l has the cardinal-intersection property at a cardinal c, then it also has the same property at any smaller cardinal a < c.

Русский

Если фильтр l обладает свойством пересечения по кардиналу c, то это свойство сохраняется и для любого меньшего кардинала a < c.

LaTeX

$$$CardinalInterFilter(l, c) \\Rightarrow (a < c) \\Rightarrow CardinalInterFilter(l, a)$$$

Lean4

theorem of_cardinalInterFilter_of_lt (l : Filter α) [CardinalInterFilter l c] {a : Cardinal.{u}} (hac : a < c) :
    CardinalInterFilter l a :=
  CardinalInterFilter.of_cardinalInterFilter_of_le l (hac.le)

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