mem_insert_of_mem

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.mem_insert_of_mem

English

If z ∈ y, then z ∈ insert x y.

Русский

Если z ∈ y, то z ∈ insert x y.

LaTeX

$$$ z \\in y \\rightarrow z \\in insert x y $$$

Lean4

theorem mem_insert_of_mem {y z : PSet} (x) (h : z ∈ y) : z ∈ insert x y :=
  mem_insert_iff.2 <| Or.inr h

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

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

Разделы

Аффилиация

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