Closedness of the functional operations

The inverse image of a closed function under a continuous linear map is closed — the closedness counterpart of convexFn_compLin, which is the convexity statement. The supporting lowerSemicontinuous_comp precomposes a lower semicontinuous g with a continuous φ; Mathlib's Continuous.comp_lowerSemicontinuous composes on the other side.

Closedness is not lower semicontinuity — ClosedFn also admits the constant ⊥ — and that branch survives precomposition because (fun _ => ⊥) ∘ A is again constant.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §5, §7.

theorem Tdaf.ConvexAnalysis.lowerSemicontinuous_comp {E : Type u_1} {G : Type u_2} [TopologicalSpace E] [TopologicalSpace G] {g : G → EReal} (hg : LowerSemicontinuous g) {φ : E → G} (hφ : Continuous φ) : LowerSemicontinuous (g ∘ φ)

Lower semicontinuity is preserved by precomposition with a continuous map.

theorem Tdaf.ConvexAnalysis.lowerSemicontinuous_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] [TopologicalSpace E] [TopologicalSpace G] {A : E →ₗ[ℝ] G} {g : G → EReal} (hg : LowerSemicontinuous g) (hA : Continuous ⇑A) : LowerSemicontinuous (compLin g A)

theorem Tdaf.ConvexAnalysis.closedFn_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace G] [IsTopologicalAddGroup G] {A : E →ₗ[ℝ] G} {g : G → EReal} (hg : ClosedFn g) (hA : Continuous ⇑A) : ClosedFn (compLin g A)

The inverse image of a closed function under a continuous linear map is closed.