ofSubsingleton

Mathlib.Data.Fintype.OfMap

URI: https://scilib.ai/kg/mathlib#Fintype.ofSubsingleton

Lean4

/-- Any subsingleton type with a witness is a fintype (with one term). -/
def ofSubsingleton (a : α) [Subsingleton α] : Fintype α :=
  ⟨{ a }, fun _ => Finset.mem_singleton.2 (Subsingleton.elim _ _)⟩
    -- In principle, this could be a `simp` theorem but it applies to any occurrence of `univ` and
    -- required unification of the (possibly very complex) `Fintype` instances.

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

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

Разделы

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

Аффилиация

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