instSetLike

Mathlib.Data.Sym.Sym2

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

Lean4

instance : SetLike (Sym2 α) α where
  coe z := {x | z.Mem x}
  coe_injective' z z'
    h := by
    simp only [Set.ext_iff, Set.mem_setOf_eq] at h
    obtain ⟨x, y⟩ := z
    obtain ⟨x', y'⟩ := z'
    have hx := h x; have hy := h y; have hx' := h x'; have hy' := h y'
    simp only [mem_iff'] at hx hy hx' hy'
    aesop

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

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

Разделы

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

Аффилиация

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