range_one — Mathlib

English

The range of the constant-one simple function on a nonempty domain is the singleton {1}.

Русский

Диапазон константной простой функции 1 на непустом множестве равен одиночке {1}.

LaTeX

$$$(1 : \\alpha \\to_{\\mathrm{S}} \\beta).\\mathrm{range} = \\{1\\}. $$$

Lean4

@[to_additive (attr := simp)]
theorem range_one [Nonempty α] [One β] : (1 : α →ₛ β).range = { 1 } :=
  Finset.ext fun x => by simp

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