A closed interval with moving endpoints is a continuous correspondence

x ↦ Set.Icc (f x) (g x) is upper and lower hemicontinuous when f and g are continuous. This is the hypothesis Berge's maximum theorem needs, and a budget set {a' | 0 ≤ a' ≤ m a} is exactly of this shape, so these two lemmas are what let a constrained consumption problem be posed as a dynamic program.

Main results

• LeanEconomics.upperHemicontinuous_Icc
• LeanEconomics.lowerHemicontinuous_Icc

The asymmetry in the hypotheses

Upper hemicontinuity needs no order hypothesis: where g x < f x the interval is empty, and the empty set is contained in everything.

Lower hemicontinuity needs f ≤ g everywhere, not merely at the point in question, and this is not a technicality. If f x = g x while f x' > g x' at nearby x', then Γ x is a single point and Γ x' is empty, so an open set meeting Γ x meets nothing nearby. Lower hemicontinuity genuinely fails there. An interval that is allowed to collapse and then vanish is not a continuous correspondence.

theorem LeanEconomics.upperHemicontinuous_Icc {X : Type u_1} [TopologicalSpace X] {f g : X → ℝ} (hf : Continuous f) (hg : Continuous g) : UpperHemicontinuous fun (x : X) => Set.Icc (f x) (g x)

An interval with continuous endpoints is upper hemicontinuous.

theorem LeanEconomics.lowerHemicontinuous_Icc {X : Type u_1} [TopologicalSpace X] {f g : X → ℝ} (hf : Continuous f) (hg : Continuous g) (hle : ∀ (x : X), f x ≤ g x) : LowerHemicontinuous fun (x : X) => Set.Icc (f x) (g x)

An interval with continuous endpoints that never collapses past emptiness is lower hemicontinuous.