notMem_sInter_of_notMem

Mathlib.SetTheory.ZFC.Basic

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

English

If y ∉ z and z ∈ x, then y ∉ ⋂₀ x.

Русский

Если y не принадлежит z и z принадлежит x, то y не принадлежит ⋂₀ x.

LaTeX

$$$ y \notin z \land z \in x \Rightarrow y \notin \bigcap_0 x $$$

Lean4

theorem notMem_sInter_of_notMem {x y z : ZFSet} (hy : y ∉ z) (hz : z ∈ x) : y ∉ ⋂₀ x := fun hx =>
  hy <| mem_of_mem_sInter hx hz

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

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

Разделы

Аффилиация

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