cardinalInter_ofCardinalInter — Mathlib

English

Instance showing that the cardinal-intersection property is preserved under taking infimum of two filters.

Русский

Инстанс показывает, что свойство пересечения по кардиналу сохраняется при взятии инфимума двух фильтров.

LaTeX

$$$CardinalInterFilter(F_1, c) \\wedge CardinalInterFilter(F_2, c) \\Rightarrow CardinalInterFilter(F_1 \\land F_2, c)$$$

Lean4

instance cardinalInter_ofCardinalInter (l : Set (Set α)) (hc : 2 < c)
    (hl : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
    CardinalInterFilter (Filter.ofCardinalInter l hc hl h_mono) c :=
  ⟨hl⟩

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