eq_pure

Mathlib.Data.Semiquot

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

← MathLib Explorer

English

q equals pure (get q p).

Русский

q равно pure (get q p).

LaTeX

$$$q = pure\ (get\ q\ p)$$$

Lean4

theorem eq_pure {q : Semiquot α} (p) : q = pure (get q p) :=
  ext.2 fun a => by simpa using ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩

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

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

Разделы

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

Аффилиация

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