theorem convexFunctionClosure_closed_properConvexFunctionOn_and_agrees_on_ri {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : (ClosedConvexFunction (convexFunctionClosure f) ∧ ProperConvexFunctionOn Set.univ (convexFunctionClosure f)) ∧ ∀ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f), convexFunctionClosure f x.ofLp = f x.ofLp