mem_of_mem_insert_of_ne

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.mem_of_mem_insert_of_ne

English

For all s and a, if x ∈ s then x ∈ insert a s.

Русский

Для всех s и a, если x ∈ s, то x ∈ insert a s.

LaTeX

$$$\forall a:\alpha\,\forall x:\alpha\, (x \in s) \Rightarrow (x \in \mathrm{insert}(a,s)).$$$

Lean4

theorem mem_of_mem_insert_of_ne : b ∈ insert a s → b ≠ a → b ∈ s :=
  Or.resolve_left

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

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

Разделы

Аффилиация

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