instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt

English

The locally constant integer-valued functions on an empty index set form a singleton.

Русский

Локально константные целочисленные функции на пустом индексе образуют одноэлементное множество.

LaTeX

$$$$\\text{LocallyConstant}\\; (\\emptyset)\\; \\mathbb{Z} \\text{ is a singleton}$$$$

Lean4

instance : Subsingleton (LocallyConstant (∅ : Set (I → Bool)) ℤ) :=
  subsingleton_iff.mpr (fun _ _ ↦ LocallyConstant.ext isEmptyElim)

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