eq_of_ne_mem

Mathlib.Data.Sym.Sym2

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

← MathLib Explorer

English

If x ≠ y and x,y ∈ z and x,y ∈ z' then z = z'.

Русский

Если x ≠ y и x,y ∈ z, x,y ∈ z', то z = z'.

LaTeX

$$$ \\text{If } x \\neq y \\text{ and } x,y \\in z \\text{ and } x,y \\in z' \\text{, then } z = z'. $$$

Lean4

theorem eq_of_ne_mem {x y : α} {z z' : Sym2 α} (h : x ≠ y) (h1 : x ∈ z) (h2 : y ∈ z) (h3 : x ∈ z') (h4 : y ∈ z') :
    z = z' :=
  ((mem_and_mem_iff h).mp ⟨h1, h2⟩).trans ((mem_and_mem_iff h).mp ⟨h3, h4⟩).symm

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

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

Разделы

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

Аффилиация

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