ContinuousOrderHom.ext

theorem ContinuousOrderHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] {f g : α →Co β}, (∀ (a : α), f a = g a) → f = g

This theorem states that for any two continuous order-preserving functions `f` and `g` from a topological space with a preorder `α` to a topological space with a preorder `β`, if for all `a` in `α`, `f(a)` is equal to `g(a)`, then `f` is equal to `g`. In other words, two continuous order-preserving functions are identical if they produce the same output for every input.

More concisely: If two continuous order-preserving functions between preordered topological spaces have the same output for every input, then they are equal.