mem_inter

Mathlib.SetTheory.ZFC.Basic

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

English

z belongs to x ∩ y iff z ∈ x and z ∈ y.

Русский

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

LaTeX

$$$ z \in x \cap y \iff z \in x \land z \in y $$$

Lean4

@[simp]
theorem mem_inter {x y z : ZFSet.{u}} : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y :=
  @mem_sep (fun z : ZFSet.{u} => z ∈ y) x z

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

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

Разделы

Аффилиация

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