eq_mk_of_mem

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.eq_mk_of_mem

Lean4

theorem eq_mk_of_mem {q : Semiquot α} {a : α} (h : a ∈ q) : q = @mk _ a q.1 h :=
  ext_s.2 rfl

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

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

Разделы

Аффилиация

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