range_one — Mathlib

English

If α is nonempty and β has a multiplicative identity, then the range of the constant-1 map 1: α → β is the singleton {1}.

Русский

Если множество α непусто и β имеет единичный элемент, образ константного отображения 1: α → β равен единице, то есть множеству {1}.

LaTeX

$$$ \operatorname{Set.range}(1 : \alpha \to \beta) = \{ 1 \}$$$

Lean4

@[to_additive (attr := simp)]
theorem range_one {α β : Type*} [One β] [Nonempty α] : Set.range (1 : α → β) = { 1 } :=
  range_const

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