English
The locally constant functions embed into continuous functions as a multiplicative monoid hom. The inclusion preserves identity and multiplication.
Русский
Локально константные функции инклюзируются в непрерывные функции как гомоморф моноида по умножению: инклюзия сохраняет единицу и произведение.
LaTeX
$$\\(LocallyConstant X Y \\to^* C(X, Y)\\) is a monoid hom, i.e. toFun preserves 1 and multiplication: toContinuousMapMonoidHom(1) = 1 and toContinuousMapMonoidHom(f g) = toContinuousMapMonoidHom(f) · toContinuousMapMonoidHom(g).$$
Lean4
/-- The inclusion of locally-constant functions into continuous functions as a multiplicative
monoid hom. -/
@[to_additive (attr := simps) /-- The inclusion of locally-constant functions into continuous
functions as an additive monoid hom. -/
]
def toContinuousMapMonoidHom [Monoid Y] [ContinuousMul Y] : LocallyConstant X Y →* C(X, Y)
where
toFun := (↑)
map_one' := by
ext
simp
map_mul' x
y := by
ext
simp
