union_mem_sup

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.union_mem_sup

← MathLib Explorer

English

If s ∈ f and t ∈ g, then their union belongs to the join of f and g.

Русский

Если S ∈ f и T ∈ g, то S ∪ T принадлежит объединению f и g.

LaTeX

$$$S \cup T \in f \sqcup g$$$

Lean4

theorem union_mem_sup {f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s ∪ t ∈ f ⊔ g :=
  ⟨mem_of_superset hs subset_union_left, mem_of_superset ht subset_union_right⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru