support_one — Mathlib

English

The support of the constant function 1: ι → R is the entire domain, i.e., every index has value 1 (and 1 ≠ 0 in R).

Русский

Опорa постоянной функции 1: ι → R равна всей областью определения; каждый индекс имеет значение 1 (и 1 ≠ 0 в R).

LaTeX

$$$ \mathrm{support}(1) = \mathrm{univ}. $$$

Lean4

@[simp]
theorem support_one : support (1 : ι → R) = univ :=
  support_const one_ne_zero

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