cardinalInterFilter_sup_eq — Mathlib

English

If l1 and l2 have a common bound c, their supremum l1 ⊔ l2 is again a CardinalInterFilter with bound c.

Русский

Если l1 и l2 имеют общее ограничение c, их верхняя выпуклость l1 ⊔ l2 снова является CardinalInterFilter с ограничением c.

LaTeX

$$$CardinalInterFilter(l_1 \sqcup l_2) c$$$

Lean4

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

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