mem_of_eq_of_mem

Mathlib.Data.Set.Basic

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

English

If x = y and y ∈ s then x ∈ s.

Русский

Если x = y и y ∈ s, то x ∈ s.

LaTeX

$$$\\forall {x y :\\ alpha} {s : Set\\alpha}, x=y \\Rightarrow (y\\in s) \\Rightarrow (x\\in s)$$$

Lean4

@[trans]
theorem mem_of_eq_of_mem {x y : α} {s : Set α} (hx : x = y) (h : y ∈ s) : x ∈ s :=
  hx.symm ▸ h

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

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

Разделы

Аффилиация

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