other_mem

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.other_mem

English

Mem.other h lies in z.

Русский

Mem.other h лежит в z.

LaTeX

$$$ \\mathrm{Mem}.other h \\in z. $$$

Lean4

theorem other_mem {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other h ∈ z :=
  by
  convert mem_mk_right a <| Mem.other h
  rw [other_spec h]

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

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

Разделы

Аффилиация

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