English
If X has the delta-generated topology, then tX equals deltaGenerated X.
Русский
Если топология X является дельта-генерированной, то tX совпадает с deltaGenerated X.
LaTeX
$$$[\\DeltaGeneratedSpace X] \\Rightarrow t_X = \\text{deltaGenerated}(X)$$$
Lean4
/-- `deltaGenerated` is idempotent as a function `TopologicalSpace X → TopologicalSpace X`. -/
theorem deltaGenerated_deltaGenerated_eq : @deltaGenerated X (deltaGenerated X) = deltaGenerated X :=
by
ext u; simp_rw [isOpen_deltaGenerated_iff];
refine
forall_congr' fun n ↦
?_
-- somewhat awkward because `ContinuousMap` doesn't play well with multiple topologies.
refine ⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩
· exact continuous_euclidean_to_deltaGenerated.mpr p.2
· exact continuous_euclidean_to_deltaGenerated.mp <| @ContinuousMap.continuous_toFun _ _ _ (_) p
