range_const — Mathlib

English

The range of the constant function is the singleton set containing that constant.

Русский

Диапазон константной функции равен синглетону, содержащему эту константу.

LaTeX

$$$\\mathrm{const}(\\alpha, b).\\mathrm{range} = \\{ b \\}$$$

Lean4

@[simp]
theorem range_const (α) [MeasurableSpace α] [Nonempty α] (b : β) : (const α b).range = { b } :=
  Finset.coe_injective <| by simp +unfoldPartialApp [Function.const]

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