theorem helperForTheorem_37_3_origin_mem_intrinsicInterior_secondDual_of_noCommonSecondRecession {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hQ : Section37Theorem37_2Qualification K) (hNoCommonSecond : ∀ (w : Fin n → ℝ), w ≠ 0 → ∃ (u : { u : Fin m → ℝ // u ∈ intrinsicInterior ℝ (effectiveDomain₁ K) }), ¬IsRecessionDirection (K ↑u) w) : 0 ∈ intrinsicInterior ℝ (effectiveDomain₂ fun (uStar : Fin m → ℝ) (x : Fin n → ℝ) => theorem37ValueSupInf K uStar x)

Helper for Theorem 37.3: condition (a) transports the origin from the ordinary interior of D* to the intrinsic interior needed by Corollary 37.1.3.

theorem helperForTheorem_37_3_origin_mem_intrinsicInterior_firstDual_of_noCommonFirstRecession {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hQ : Section37Theorem37_2Qualification K) (hNoCommonFirst : ∀ (z : Fin m → ℝ), z ≠ 0 → ∃ (v : { v : Fin n → ℝ // v ∈ intrinsicInterior ℝ (effectiveDomain₂ K) }), ¬IsRecessionDirection (fun (u : Fin m → ℝ) => -K u ↑v) z) : 0 ∈ intrinsicInterior ℝ (effectiveDomain₁ fun (uStar : Fin m → ℝ) (x : Fin n → ℝ) => theorem37ValueSupInf K uStar x)

Helper for Theorem 37.3: condition (b) transports the origin from the ordinary interior of C* to the intrinsic interior needed by Corollary 37.1.3.

theorem helperForTheorem_37_3_finiteSaddleValue_of_bothNoCommonRecessionConditions {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hQ : Section37Theorem37_2Qualification K) (hNoCommonSecond : ∀ (w : Fin n → ℝ), w ≠ 0 → ∃ (u : { u : Fin m → ℝ // u ∈ intrinsicInterior ℝ (effectiveDomain₁ K) }), ¬IsRecessionDirection (K ↑u) w) (hNoCommonFirst : ∀ (z : Fin m → ℝ), z ≠ 0 → ∃ (v : { v : Fin n → ℝ // v ∈ intrinsicInterior ℝ (effectiveDomain₂ K) }), ¬IsRecessionDirection (fun (u : Fin m → ℝ) => -K u ↑v) z) : minimaxValue K ≠ ⊤ ∧ minimaxValue K ≠ ⊥

Helper for Theorem 37.3: when both recession-direction conditions hold, Corollary 37.1.3 gives finiteness of the common saddle-value.

theorem section37_theorem37_3 {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hQ : Section37Theorem37_2Qualification K) : have C := effectiveDomain₁ K; have D := effectiveDomain₂ K; ((∀ (w : Fin n → ℝ), w ≠ 0 → ∃ (u : { u : Fin m → ℝ // u ∈ intrinsicInterior ℝ C }), ¬IsRecessionDirection (K ↑u) w) ∨ ∀ (z : Fin m → ℝ), z ≠ 0 → ∃ (v : { v : Fin n → ℝ // v ∈ intrinsicInterior ℝ D }), ¬IsRecessionDirection (fun (u : Fin m → ℝ) => -K u ↑v) z) → minimaxValue K = maximinValue K ∧ (((∀ (w : Fin n → ℝ), w ≠ 0 → ∃ (u : { u : Fin m → ℝ // u ∈ intrinsicInterior ℝ C }), ¬IsRecessionDirection (K ↑u) w) ∧ ∀ (z : Fin m → ℝ), z ≠ 0 → ∃ (v : { v : Fin n → ℝ // v ∈ intrinsicInterior ℝ D }), ¬IsRecessionDirection (fun (u : Fin m → ℝ) => -K u ↑v) z) → minimaxValue K ≠ ⊤ ∧ minimaxValue K ≠ ⊥)

Theorem 37.3: either recession-direction condition from Corollary 37.2.1 implies existence of the saddle-value of K, and if both hold then this common value is finite.