union_def

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.union_def

English

The union of two sets is the set of elements belonging to either set.

Русский

Объединение двух множеств состоит из элементов, принадлежащих как одному, так и другому множеству.

LaTeX

$$$(s_1 \cup s_2) = \{ a \mid a \in s_1 \lor a \in s_2 \}$$$

Lean4

theorem union_def {s₁ s₂ : Set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂} :=
  rfl

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

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

Разделы

Аффилиация

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