union_mem_sups

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.union_mem_sups

English

If s ∈ 𝒜 and t ∈ ℬ, then their union lies in 𝒜 ⊻ ℬ: s ∈ 𝒜 ∧ t ∈ ℬ ⇒ s ∪ t ∈ 𝒜 ⊻ ℬ.

Русский

Если s принадлежит 𝒜, а t принадлежит ℬ, то их объединение принадлежит 𝒜 ⊻ ℬ.

LaTeX

$$$ s \in 𝒜 \to t \in ℬ \to s \cup t \in 𝒜 \vee ℬ $$$

Lean4

theorem union_mem_sups : s ∈ 𝒜 → t ∈ ℬ → s ∪ t ∈ 𝒜 ⊻ ℬ :=
  sup_mem_sups

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

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

Разделы

Аффилиация

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