ContinuousOpenMap.ext

theorem ContinuousOpenMap.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α →CO β}, (∀ (a : α), f a = g a) → f = g

This theorem states that for any two continuous open maps `f` and `g` from a topological space `α` to another topological space `β`, if they map every point in `α` to the same point in `β`, then `f` and `g` must be the same continuous open map. This means that continuous open maps are uniquely defined by how they map every individual point from `α` to `β`.

More concisely: If two continuous open maps from one topological space to another map every point to the same image, then they are equal as functions.