pure_inj

Mathlib.Data.Semiquot

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

English

q equals pure of its get value: q = pure (get q p).

Русский

q равно чистому значению get q p: q = pure (get q p).

LaTeX

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

Lean4

@[simp]
theorem pure_inj {a b : α} : (pure a : Semiquot α) = pure b ↔ a = b :=
  ext_s.trans Set.singleton_eq_singleton_iff

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

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

Разделы

Аффилиация

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