IsMaxOn.closure

theorem IsMaxOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y] [inst_3 : OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X}, IsMaxOn f s a → ContinuousOn f (closure s) → IsMaxOn f (closure s) a

The theorem `IsMaxOn.closure` states that for all topological spaces `X` and `Y`, where `Y` also has a preorder structure and an order-closed topology, given a function `f : X → Y`, a set `s : Set X` and a point `a : X`, if `f` reaches its maximum at `a` over the set `s` and `f` is continuous on the closure of `s`, then `f` also reaches its maximum at `a` over the closure of `s`. This means that the continuity of `f` on the closure of `s` preserves the property of `f` having its maximum value at `a`.

More concisely: If `f : X → Y` is a continuous function from a topological space `X` to a topological preorder space `Y`, `s ⊆ X` is a set, `a ∈ X` is a point, and `f(a)` is the maximum value of `f` over `s`, then `f(a)` is also the maximum value of `f` over the closure of `s`.