one — Mathlib

English

The unit set in the Pointwise context is the singleton {1}.

Русский

Единичное множество в контексте точечных операций есть единичное множество {1}.

LaTeX

$$The set 1 is defined as the singleton {1} in the Pointwise context: 1 = {1}.$$

Lean4

/-- The set `1 : Set α` is defined as `{1}` in scope `Pointwise`. -/
@[to_additive /-- The set `0 : Set α` is defined as `{0}` in scope `Pointwise`. -/
    ]
protected def one : One (Set α) :=
  ⟨{ 1 }⟩

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