continuous_pi_iff — Mathlib

English

A function f: X → ∏ i A_i is continuous if and only if each coordinate f i is continuous: ∀i, Continuous fun a => f a i.

Русский

Функция f: X → ∏_i A_i непрерывна тогда и только тогда, когда каждая координата f_i непрерывна: ∀i, Continuous (λ a, f a i).

LaTeX

$$$$ \operatorname{Continuous}(f) \iff \forall i, \operatorname{Continuous}(\lambda a. f(a)_i) $$$$

Lean4

theorem continuous_pi_iff : Continuous f ↔ ∀ i, Continuous fun a => f a i := by
  simp only [continuous_iInf_rng, continuous_induced_rng, comp_def]

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