Infima of a lower semicontinuous function over a compact factor

A lower semicontinuous function on a nonempty compact space attains its infimum, and the partial infimum y ↦ ⨅ x, f (x, y) of a jointly lower semicontinuous function over a compact first factor is again lower semicontinuous.

The first statement is recorded here as an equation rather than as IsMinOn because that is the form the second needs: proving lower semicontinuity means turning a strict lower bound valid at every point of the compact factor into a strict lower bound for the infimum itself, and attainment is what performs that step. Only lower semicontinuity of f is used, so no continuity, metrizability or countability hypothesis appears, and the order β carries no topology of its own.

Mathlib has LowerSemicontinuousOn.exists_isMinOn, the extreme value theorem for lower semicontinuous functions, but nothing about infima over a compact factor of a product: its semicontinuity operations combine functions on a fixed domain, and the corresponding lowerSemicontinuous_iInf is false without compactness: arbitrary infima do not preserve lower semicontinuity. What an infimum does preserve is upper semicontinuity, of upper semicontinuous and in particular of continuous functions, which is upperSemicontinuous_iInf.

Main results

• TauCeti.exists_iInf_eq_of_lowerSemicontinuous: on a nonempty compact space, a lower semicontinuous function attains its infimum.
• TauCeti.lowerSemicontinuous_iInf_of_compactSpace: the partial infimum of a jointly lower semicontinuous function over a compact first factor is lower semicontinuous.

theorem TauCeti.exists_iInf_eq_of_lowerSemicontinuous {X : Type u_1} {β : Type u_3} [TopologicalSpace X] [CompleteLinearOrder β] [CompactSpace X] [Nonempty X] {f : X → β} (hf : LowerSemicontinuous f) : ∃ (x₀ : X), ⨅ (x : X), f x = f x₀

A lower semicontinuous function on a nonempty compact space attains its infimum.

theorem TauCeti.lowerSemicontinuous_iInf_of_compactSpace {X : Type u_1} {Y : Type u_2} {β : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CompleteLinearOrder β] [CompactSpace X] {f : X × Y → β} (hf : LowerSemicontinuous f) : LowerSemicontinuous fun (y : Y) => ⨅ (x : X), f (x, y)

The infimum of a jointly lower semicontinuous function over a compact first factor is a lower semicontinuous function of the second variable.

Compactness is what makes this true: an arbitrary infimum of lower semicontinuous functions need not be lower semicontinuous.