continuous on an open set

Stream: Is there code for X?

[Yaël Dillies]

Is it true that a function is continuous on a given open set iff it's continuous (not within) at all points in the set? If so, do we have this somewhere?

import topology.subset_properties

variables {α β : Type*} [topological_space α] [topological_space β] {s : set α} {f : α → β}

lemma is_open.continuous_on_iff (hs : is_open s) :
  continuous_on f s ↔ ∀ ⦃a⦄, a ∈ s → continuous_at f a := sorry

[Adam Topaz]

it is indeed true:

lemma is_open.continuous_on_iff (hs : is_open s) :
  continuous_on f s ↔ ∀ ⦃a⦄, a ∈ s → continuous_at f a :=
⟨λ h a ha, h.continuous_at (is_open.mem_nhds hs ha), λ h, continuous_at.continuous_on h⟩

[Jireh Loreaux]

docs#continuous_on_open_iff looks close, but not quite there.

[Moritz Doll]

lemma is_open.continuous_on_iff (hs : is_open s) :
  continuous_on f s ↔ ∀ ⦃a⦄, a ∈ s → continuous_at f a :=
ball_congr (λ _, continuous_within_at_iff_continuous_at ∘ hs.mem_nhds)

[Moritz Doll]

(deleted)

[Moritz Doll]

it's a shame that the first argument in the forall is explicit,
ball_congr $ continuous_within_at_iff_continuous_at ∘ hs.mem_nhds would be a beautiful proof

[Yaël Dillies]

Great thanks! Do you think this is worth being a lemma or am I going against the library design by doing this?

[Patrick Massot]

This is a very reasonable lemma. If it isn't there already then it should definitely be added.

[Yaël Dillies]

The greater context is that I'm proving that a convex function on a finite dimensional real normed space is continuous, and I was contemplating stating it as convex_on ℝ s f → continuous_on f (interior s) vs convex_on ℝ s f → ∀ a ∈ interior s, continuous_at f a .