instContinuousEval — Mathlib

English

If A is LocallyCompactPair with B, then evaluation is continuous for ContinuousMonoidHom A B.

Русский

Если пары A,B образуют локально компактную пару, то функция оценки непрерывна для ContinuousMonoidHom A B.

LaTeX

$$$\text{ContinuousEval}(\mathrm{ContinuousMonoidHom}(A,B),A,B)$ при условии LocallyCompactPair A B.$$

Lean4

@[to_additive]
instance instContinuousEval [LocallyCompactPair A B] : ContinuousEval (ContinuousMonoidHom A B) A B :=
  .of_continuous_forget (isInducing_toContinuousMap A B).continuous

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