of_cardinalInterFilter_of_le — Mathlib

English

If l is a CardinalInterFilter with a, and a ≤ c, then there is a CardinalInterFilter l a.

Русский

Если фильтр l имеет CardinalInterFilter с a и a ≤ c, то существует CardinalInterFilter l a.

LaTeX

$$$$ (l : Filter α) [CardinalInterFilter l c] (hac : a \\le c) \\Rightarrow CardinalInterFilter l a $$$$

Lean4

/-- Every CardinalInterFilter for some c also is a CardinalInterFilter for some a ≤ c -/
theorem of_cardinalInterFilter_of_le (l : Filter α) [CardinalInterFilter l c] {a : Cardinal.{u}} (hac : a ≤ c) :
    CardinalInterFilter l a where
  cardinal_sInter_mem S hS a := CardinalInterFilter.cardinal_sInter_mem S (lt_of_lt_of_le hS hac) a

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