mulIndicator_one' — Mathlib

English

For any set S ⊆ α, the function x ↦ 1 is equal to the indicator of S evaluated at the constant function 1; i.e. the indicator of S with value 1 is the constant-1 function.

Русский

Пусть S ⊆ α. Функция x ↦ 1 совпадает с индикаторной функцией S, применённой к константе 1; то есть знаковая функция единицы на S равна константе 1 на всей области.

LaTeX

$$$s\\mulIndicator(1 : \\alpha \\to M) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_one' {s : Set α} : s.mulIndicator (1 : α → M) = 1 :=
  mulIndicator_one M s

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