right_mem_of_mk_mem_sym2

Mathlib.Data.List.Sym

URI: https://scilib.ai/kg/mathlib#List.right_mem_of_mk_mem_sym2

← MathLib Explorer

English

If s(a,b) appears in xs.sym2, then b belongs to xs.

Русский

Если s(a,b) встречается в xs.sym2, то b ∈ xs.

LaTeX

$$$$ s(a,b) \\in xs.sym2 \\Rightarrow b \\in xs $$$$

Lean4

theorem right_mem_of_mk_mem_sym2 {xs : List α} {a b : α} (h : s(a, b) ∈ xs.sym2) : b ∈ xs :=
  by
  rw [Sym2.eq_swap] at h
  exact left_mem_of_mk_mem_sym2 h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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