theorem riEpigraph_section_mem_iff {n : ℕ} {f : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) (μ : ℝ) : have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); have y := (EuclideanSpace.equiv (Fin n) ℝ).symm x; have z := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => μ; have Cy := fun (y : EuclideanSpace ℝ (Fin n)) => {z : EuclideanSpace ℝ (Fin 1) | (appendAffineEquiv n 1) (y, z) ∈ C}; z ∈ Cy y ↔ f x ≤ ↑μ

The vertical section of the embedded epigraph corresponds to the usual inequality.