mem_or_mem_of_mem_union

Mathlib.Data.Set.Basic

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

English

From x ∈ a ∪ b, conclude x ∈ a ∨ x ∈ b.

Русский

Из x ∈ a ∪ b следует x ∈ a или x ∈ b.

LaTeX

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

Lean4

theorem mem_or_mem_of_mem_union {x : α} {a b : Set α} (H : x ∈ a ∪ b) : x ∈ a ∨ x ∈ b :=
  H

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

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

Разделы

Аффилиация

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