mem_union

Mathlib.Data.Set.Basic

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

English

For every x, x ∈ a ∪ b iff x ∈ a or x ∈ b.

Русский

Для любого x верно: x ∈ a ∪ b тогда и только тогда, когда x ∈ a или x ∈ b.

LaTeX

$$$x \in a \cup b \iff x \in a \lor x \in b$$$

Lean4

@[simp, grind =]
theorem mem_union (x : α) (a b : Set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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