mem_union

Mathlib.Data.List.AList

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

English

Membership in the union equals membership in either part.

Русский

Членство в объединении равно членству либо в первом, либо во втором компоненте.

LaTeX

$$$ a \in s_1 \cup s_2 \iff a \in s_1 \lor a \in s_2 $$$

Lean4

@[simp]
theorem mem_union {a} {s₁ s₂ : AList β} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ :=
  mem_keys_kunion

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

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

Разделы

Аффилиация

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