pow — Mathlib

English

For any f: X → M and any natural n, the map b ↦ f(b)^n is continuous whenever f is continuous.

Русский

Пусть f: X → M непрерывна; тогда для любого натурального n отображение b ↦ f(b)^n непрерывно.

LaTeX

$$$\\forall f:\\, X \\to M,\\;\\text{Continuous } f \\Rightarrow \\forall n \\in \\mathbb{N},\\;\\text{Continuous}(b \\mapsto f(b)^n)$$$

Lean4

@[to_additive (attr := aesop safe -100 (rule_sets := [Continuous]), fun_prop)]
theorem pow {f : X → M} (h : Continuous f) (n : ℕ) : Continuous fun b => f b ^ n :=
  (continuous_pow n).comp h

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