theorem ERealFunction.mem_gamma_comp_continuousLinearMap {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (f : K → EReal) (L : H →L[ℝ] K) (hf : f ∈ Γ(K)) : f ∘ ⇑L ∈ Γ(H)

Precomposing a member of gamma K with a continuous linear map yields a member of gamma H.

theorem ERealFunction.isProper_comp_continuousLinearMap_of_dom_inter_range_nonempty {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (f : K → EReal) (L : H →L[ℝ] K) (hf_proper : IsProper f) (hdom : (dom f ∩ Set.range ⇑L).Nonempty) : IsProper (f ∘ ⇑L)

If dom f meets the range of L, then precomposition with L preserves properness.

theorem ERealFunction.isProper_and_mem_gamma_comp_continuousLinearMap_of_dom_inter_range_nonempty {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (f : K → EReal) (L : H →L[ℝ] K) (hf_proper : IsProper f) (hf_gamma : f ∈ Γ(K)) (hdom : (dom f ∩ Set.range ⇑L).Nonempty) : IsProper (f ∘ ⇑L) ∧ f ∘ ⇑L ∈ Γ(H)

Proposition 9.5: if f is proper, lower semicontinuous, and convex on K, and dom f meets the range of a continuous linear map L : H →L[ℝ] K, then f ∘ L is proper, lower semicontinuous, and convex on H.