English
Let X be a delta-generated space and Y a topological space. A map f: X → Y is continuous if and only if for every n ∈ ℕ and every continuous p: ℝ^n → X, the composition f ∘ p: ℝ^n → Y is continuous.
Русский
Пусть X – дельта-генерируемое пространство, Y – топологическое пространство. Отображение f: X → Y непрерывно тогда и только тогда, когда для каждого n ∈ ℕ и каждого непрерывного p: ℝ^n → X композиция f ∘ p: ℝ^n → Y непрерывна.
LaTeX
$$$$\text{Continuous}(f) \iff \forall n \in \mathbb{N}, \forall p:\mathbb{R}^n \to X,\ \text{Continuous}(p) \Rightarrow \text{Continuous}(f \circ p).$$$$
Lean4
/-- A map out of a delta-generated space is continuous iff it preserves continuity of maps
from ℝⁿ into X. -/
theorem continuous_iff [DeltaGeneratedSpace X] {f : X → Y} :
Continuous f ↔ ∀ (n : ℕ) (p : C(((Fin n) → ℝ), X)), Continuous (f ∘ p) :=
by
simp_rw [continuous_iff_coinduced_le]
nth_rewrite 1 [eq_deltaGenerated (X := X), deltaGenerated]
simp [coinduced_compose, Sigma.forall]
