of_subsingleton — Mathlib

English

A subsingleton type is finite (trivially has at most one element).

Русский

Тип с Subsingleton свойством конечно: в нём не более одного элемента.

LaTeX

$$$\text{Subsingleton}(\alpha) \Rightarrow \operatorname{Finite}(\alpha).$$$

Lean4

instance (priority := 100) of_subsingleton {α : Sort*} [Subsingleton α] : Finite α :=
  Finite.of_injective (Function.const α ()) <|
    Function.injective_of_subsingleton
      _
        -- Higher priority for `Prop`s

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