countableInterFilter_sup — Mathlib

English

Supremum (least upper bound) of two CountableInterFilters l1 and l2 is CountableInterFilter (l1 ⊔ l2).

Русский

Супремум двух CountableInterFilter даёт CountableInterFilter для l1 ⊔ l2.

LaTeX

$$$\\text{countableInterFilter_sup}(l_1, l_2) : CountableInterFilter (l_1 \\ ⊔ \\ l_2)$$$

Lean4

/-- Supremum of two `CountableInterFilter`s is a `CountableInterFilter`. -/
instance countableInterFilter_sup (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] :
    CountableInterFilter (l₁ ⊔ l₂) :=
  by
  refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩ <;> refine (countable_sInter_mem hSc).2 fun s hs => ?_
  exacts [(hS s hs).1, (hS s hs).2]

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