continuous_of_continuous_uncurry — Mathlib

English

If f: A → ContinuousMonoidHom B C has the uncurried map continuous, then f is continuous.

Русский

Если f: A → ContinuousMonoidHom B C имеет непрерывную раскоррекцию (uncurry), то f непрерывна.

LaTeX

$$$\text{If } f: A \to \mathrm{ContinuousMonoidHom}(B,C) \text{ and } \text{uncurry } (f) \text{ is continuous, then } f \text{ is continuous.}$$$

Lean4

@[to_additive]
theorem continuous_of_continuous_uncurry {A : Type*} [TopologicalSpace A] (f : A → ContinuousMonoidHom B C)
    (h : Continuous (Function.uncurry fun x y => f x y)) : Continuous f :=
  (isInducing_toContinuousMap _ _).continuous_iff.mpr (ContinuousMap.continuous_of_continuous_uncurry _ h)

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