isPure_univ

Mathlib.Data.Semiquot

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

← MathLib Explorer

English

IsPure univ is equivalent to Subsingleton α when α is inhabited.

Русский

IsPure univ эквивалентно Subsingleton α при условии существования элемента в α.

LaTeX

$$$\mathrm{IsPure}(\mathrm{univ}) \iff \mathrm{Subsingleton}(\alpha)$$$

Lean4

@[simp]
theorem isPure_univ [Inhabited α] : @IsPure α univ ↔ Subsingleton α :=
  ⟨fun h => ⟨fun a b => h a trivial b trivial⟩, fun ⟨h⟩ a _ b _ => h a b⟩

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

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

Разделы

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

Аффилиация

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