instSubsingletonTerminalType — Mathlib

English

A type X is terminal if and only if it has exactly one element; equivalently, IsTerminal X holds if and only if Unique X holds.

Русский

Тип X является терминальным тогда и только тогда, когда в нём ровно один элемент; эквивалентно: IsTerminal X выполняется тогда и только тогда, когда существует ровно один элемент в X.

LaTeX

$$$$ IsTerminal\\,X \\quad\\text{эквивелентно}\\quad Unique\\,X $$$$

Lean4

instance : Subsingleton (⊤_ (Type u)) :=
  ⟨fun a b => congr_fun (@Subsingleton.elim (_ ⟶ ⊤_ (Type u)) _ (fun _ => a) (fun _ => b)) (ULift.up (0 : Fin 1))⟩

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