existsUnique_eq'

Mathlib.Logic.ExistsUnique

URI: https://scilib.ai/kg/mathlib#existsUnique_eq'

← MathLib Explorer

English

There exists exactly one a with a' = a.

Русский

Существует ровно один элемент a такой, что a' = a.

LaTeX

$$$$ \\exists! a, a' = a. $$$$

Lean4

/-- The difference with `existsUnique_eq` is that the equality is reversed. -/
@[simp]
theorem existsUnique_eq' {a' : α} : ∃! a, a' = a := by simp only [ExistsUnique, and_self, forall_eq', exists_eq']

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

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

Разделы

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

Аффилиация

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