mem_union

Mathlib.SetTheory.ZFC.Basic

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

English

z belongs to x ∪ y iff z ∈ x or z ∈ y.

Русский

z принадлежит x ∪ y тогда, когда z ∈ x или z ∈ y.

LaTeX

$$$ z \in x \cup y \iff z \in x \lor z \in y $$$

Lean4

@[simp]
theorem mem_union {x y z : ZFSet.{u}} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y :=
  by
  rw [← mem_toSet]
  simp

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

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

Разделы

Аффилиация

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