English
If l1 and l2 are filters on α each equipped with a cardinal-interfilter bound c1 and c2, then their infimum l1 ⊓ l2 also carries a cardinal-interfilter bound c1 ⊓ c2.
Русский
Если l1 и l2 — фильтры на α и для каждого дано соответствующее кардинально-интерфильтрогBound c1 и c2, то ихInfimum l1 ⊓ l2 также имеет кардинально-интерфильтр c1 ⊓ c2.
LaTeX
$$$CardinalInterFilter(l_1 \sqcap l_2) (c_1 \sqcap c_2)$$$
Lean4
instance cardinalInterFilter_inf (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁]
[CardinalInterFilter l₂ c₂] : CardinalInterFilter (l₁ ⊓ l₂) (c₁ ⊓ c₂) :=
by
have : CardinalInterFilter l₁ (c₁ ⊓ c₂) := CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
have : CardinalInterFilter l₂ (c₁ ⊓ c₂) := CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
exact cardinalInterFilter_inf_eq _ _
