Commit 2026-11-10 23:17 2f98fa8f

chore(Topology/Connected/TotallyDisconnected): use a typeclass param in PreconnectedSpace.constant and respell using IsConst (#45848) Before:

theorem PreconnectedSpace.constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y]
    (hp : PreconnectedSpace α) {f : α → Y} (hf : Continuous f) {x y : α} : f x = f y :=

After:

theorem Continuous.isConst_of_preconnectedSpace {Y : Type*} [TopologicalSpace Y]
    [DiscreteTopology Y] [PreconnectedSpace α] {f : α → Y} (hf : Continuous f) : f.IsConst :=