English
Let X be a delta-generated space. A map f: X → Y is continuous with respect to the delta-generated topology on Y if and only if f is continuous in the usual sense.
Русский
Пусть X – дельта-генерируемое пространство. Отображение f: X → Y непрерывно относительно δ-генерированной топологии на Y тогда и только тогда, когда оно непрерывно в обычном смысле.
LaTeX
$$$$\text{Continuous}_{\delta\text{Gen}(Y)}(f) \iff \text{Continuous}(f).$$$$
Lean4
/-- A map out of a delta-generated space is continuous iff it is continuous with respect
to the delta-generated topology on the codomain. -/
theorem continuous_to_deltaGenerated [DeltaGeneratedSpace X] {f : X → Y} :
Continuous[_, deltaGenerated Y] f ↔ Continuous f := by
simp_rw [DeltaGeneratedSpace.continuous_iff, continuous_euclidean_to_deltaGenerated]
