theorem innerProductEquation_of_fullDomain_or_closed_fullAdjointDomain {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} : IsGraphConvexBifunction F → HasNoBotValuesBifunction F → (convexBifunctionDomains F).1 = Set.univ ∨ IsFunctionConvexClosed (graphFunctionOfBifunction F) ∧ (convexBifunctionDomains F).2 = Set.univ → HasInnerProductEquation F

Corollary33.0.40 (Sufficient conditions for the global pairing identity): the primal pairing and genuine-adjoint pairing agree everywhere if either the primal domain is full, or the graph function is convex-closed and the genuine adjoint domain is full.

theorem helperForCorollary33_0_41_exists_off_first_domain {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hdom : (convexBifunctionDomains F).1 ≠ Set.univ) : ∃ (u : Fin m → ℝ), u ∉ (convexBifunctionDomains F).1

Helper for Corollary33.0.41: a proper first convex-bifunction domain component omits some primal parameter.

theorem helperForCorollary33_0_41_exists_off_second_domain {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hdomAdj : (convexBifunctionDomains F).2 ≠ Set.univ) : ∃ (xStar : Fin n → ℝ), xStar ∉ (convexBifunctionDomains F).2

Helper for Corollary33.0.41: a proper second convex-bifunction domain component omits some dual vector.

theorem helperForCorollary33_0_41_contradiction_at_off_domain_point {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {xStar : Fin n → ℝ} (hInner : HasInnerProductEquation F) (huOutside : u ∉ (convexBifunctionDomains F).1) (hxOutside : xStar ∉ (convexBifunctionDomains F).2) : False

Helper for Corollary33.0.41: the inner-product equation fails at any point lying outside both convex-bifunction domain components.

theorem not_hasInnerProductEquation_of_nonfull_domains {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} : (convexBifunctionDomains F).1 ≠ Set.univ → (convexBifunctionDomains F).2 ≠ Set.univ → ¬HasInnerProductEquation F

Corollary33.0.41 (Failure when both domains are not full): if neither the primal domain nor the genuine adjoint domain is all of space, then the global pairing identity cannot hold.

theorem helperForTheorem33_0_39_domainDichotomy_of_innerProductEquation {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hInner : HasInnerProductEquation F) : (convexBifunctionDomains F).1 = Set.univ ∨ (convexBifunctionDomains F).2 = Set.univ

Helper for Theorem33.0.39: the genuine inner-product equation forces at least one of the two domain components to be all of space.

theorem helperForCorollary33_3_1_rockafellarConvex_and_graphFunctionClosed_of_closedConvexWitness {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hNoBot : HasNoBotValuesBifunction F) : IsGraphConvexBifunction F ∧ IsFunctionConvexClosed (graphFunctionOfBifunction F)

Helper for Corollary33.3.1: a closed convex witness with no ⊥ values already supplies the Rockafellar convexity and graph-closure data needed by the coordinatewise-closure machinery.

noncomputable def canonicalConcaveClosureInFirst {m n : ℕ} (K : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

Canonical Chapter 2 closure in the first (concave) coordinate. This is kept distinct from the older ball-based raw closure, which need not agree on improper sections.

noncomputable def canonicalConvexClosureInSecond {m n : ℕ} (K : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

Canonical Chapter 2 closure in the second (convex) coordinate.

theorem helperForCorollary33_3_1_coordinatewise_closure_pair_of_closedConvexWitness {m n : ℕ} {K Kbar F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hNoBot : HasNoBotValuesBifunction F) (hPair : ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), K u xStar = convexBifunctionPairing F u xStar) (hAdj : ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), Kbar u xStar = convexBifunctionCanonicalAdjointPairing F xStar u) : Kbar = canonicalConcaveClosureInFirst K ∧ canonicalConvexClosureInSecond Kbar = K

Helper for Corollary33.3.1: a closed convex bifunction witness with no ⊥ values forces the canonical coordinatewise closure identities for the represented pairing kernels.

theorem helperForCorollary33_3_1_coordinatewise_closure_pair_of_closedConvexWitnessPackage {m n : ℕ} {K Kbar F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hWitness : ClosedConvexBifunction F ∧ HasNoBotValuesBifunction F ∧ (∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), K u xStar = convexBifunctionPairing F u xStar) ∧ ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), Kbar u xStar = convexBifunctionCanonicalAdjointPairing F xStar u) : Kbar = canonicalConcaveClosureInFirst K ∧ canonicalConvexClosureInSecond Kbar = K

Helper for Corollary33.3.1: the forward implication only uses the packaged closed convex witness data, so it can be invoked directly from the existential interface used in the corollary statement.

theorem helperForCorollary33_3_1_coordinatewise_closure_pair_of_closedConvexUniqueWitness {m n : ℕ} {K Kbar : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hExists : ∃! F : (Fin m → ℝ) → (Fin n → ℝ) → EReal, ClosedConvexBifunction F ∧ HasNoBotValuesBifunction F ∧ (∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), K u xStar = convexBifunctionPairing F u xStar) ∧ ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), Kbar u xStar = convexBifunctionCanonicalAdjointPairing F xStar u) : Kbar = canonicalConcaveClosureInFirst K ∧ canonicalConvexClosureInSecond Kbar = K

Helper for Corollary33.3.1: the unique-existence hypothesis in the corollary statement still yields the same coordinatewise closure pair after discarding uniqueness.

theorem helperForCorollary33_3_2_firstVariableSection_isConcaveAndConvex_of_simultaneousOrientations {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK : IsConcaveConvexOn Set.univ Set.univ K) (hVC : IsConvexConcaveOn Set.univ Set.univ K) (xStar : Fin n → ℝ) : (IsERealConcaveOn Set.univ fun (u : Fin m → ℝ) => K u xStar) ∧ IsERealConvexOn Set.univ fun (u : Fin m → ℝ) => K u xStar

Helper for Corollary33.3.2: simultaneous concave-convex and convex-concave structure on a kernel makes every first-variable section simultaneously concave and convex.

theorem helperForCorollary33_3_2_secondVariableSection_isConvexAndConcave_of_simultaneousOrientations {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK : IsConcaveConvexOn Set.univ Set.univ K) (hVC : IsConvexConcaveOn Set.univ Set.univ K) (u : Fin m → ℝ) : (IsERealConvexOn Set.univ fun (xStar : Fin n → ℝ) => K u xStar) ∧ IsERealConcaveOn Set.univ fun (xStar : Fin n → ℝ) => K u xStar

Helper for Corollary33.3.2: simultaneous concave-convex and convex-concave structure on a kernel makes every second-variable section simultaneously convex and concave.

theorem helperForCorollary33_3_2_allFirstVariableSections_areConcaveAndConvex {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK : IsConcaveConvexOn Set.univ Set.univ K) (hVC : IsConvexConcaveOn Set.univ Set.univ K) (xStar : Fin n → ℝ) : (IsERealConcaveOn Set.univ fun (u : Fin m → ℝ) => K u xStar) ∧ IsERealConvexOn Set.univ fun (u : Fin m → ℝ) => K u xStar

Helper for Corollary33.3.2: the simultaneous orientation hypotheses package the first-variable section orientations uniformly over all frozen dual vectors.

theorem helperForCorollary33_3_2_allSecondVariableSections_areConvexAndConcave {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK : IsConcaveConvexOn Set.univ Set.univ K) (hVC : IsConvexConcaveOn Set.univ Set.univ K) (u : Fin m → ℝ) : (IsERealConvexOn Set.univ fun (xStar : Fin n → ℝ) => K u xStar) ∧ IsERealConcaveOn Set.univ fun (xStar : Fin n → ℝ) => K u xStar

Helper for Corollary33.3.2: the simultaneous orientation hypotheses package the second-variable section orientations uniformly over all frozen primal vectors.

theorem helperForCorollary33_3_2_allSections_have_simultaneousOrientations {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK : IsConcaveConvexOn Set.univ Set.univ K) (hVC : IsConvexConcaveOn Set.univ Set.univ K) : (∀ (xStar : Fin n → ℝ), (IsERealConcaveOn Set.univ fun (u : Fin m → ℝ) => K u xStar) ∧ IsERealConvexOn Set.univ fun (u : Fin m → ℝ) => K u xStar) ∧ ∀ (u : Fin m → ℝ), (IsERealConvexOn Set.univ fun (xStar : Fin n → ℝ) => K u xStar) ∧ IsERealConcaveOn Set.univ fun (xStar : Fin n → ℝ) => K u xStar

Helper for Corollary33.3.2: simultaneous concave-convex and convex-concave structure on a kernel packages both first-variable and second-variable section orientations at once.

theorem helperForCorollary33_3_3_realKernel_hasNoTopOrBotValues {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} : HasNoTopOrBotValuesBifunction fun (u : Fin m → ℝ) (xStar : Fin n → ℝ) => ↑(K u xStar)

Helper for Corollary33.3.3: a real-valued kernel, viewed in EReal, satisfies both one-sided finiteness conventions required by the saddle-function correspondence.

theorem helperForCorollary33_3_3_lowerSimpleExtension_le_upperSimpleExtension {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (u : Fin m → ℝ) (xStar : Fin n → ℝ) : lowerSimpleExtension C D K u xStar ≤ upperSimpleExtension C D K u xStar

Helper for Corollary33.3.3: every lower simple extension lies pointwise below the corresponding upper simple extension.

theorem helperForCorollary33_3_3_simpleExtensions_of_real_agree_on_product {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {u : Fin m → ℝ} {xStar : Fin n → ℝ} (hu : u ∈ C) (hxStar : xStar ∈ D) : lowerSimpleExtension C D (fun (u' : Fin m → ℝ) (xStar' : Fin n → ℝ) => ↑(K u' xStar')) u xStar = ↑(K u xStar) ∧ upperSimpleExtension C D (fun (u' : Fin m → ℝ) (xStar' : Fin n → ℝ) => ↑(K u' xStar')) u xStar = ↑(K u xStar)

Helper for Corollary33.3.3: on C × D, the simple extensions of a real-valued kernel agree with the original kernel after coercion to EReal.

theorem helperForCorollary33_3_3_realKernel_simpleExtensions_areOrdered_and_agreeOnProduct {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} : (∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), lowerSimpleExtension C D (fun (u' : Fin m → ℝ) (xStar' : Fin n → ℝ) => ↑(K u' xStar')) u xStar ≤ upperSimpleExtension C D (fun (u' : Fin m → ℝ) (xStar' : Fin n → ℝ) => ↑(K u' xStar')) u xStar) ∧ ∀ ⦃u : Fin m → ℝ⦄ ⦃xStar : Fin n → ℝ⦄, u ∈ C → xStar ∈ D → lowerSimpleExtension C D (fun (u' : Fin m → ℝ) (xStar' : Fin n → ℝ) => ↑(K u' xStar')) u xStar = ↑(K u xStar) ∧ upperSimpleExtension C D (fun (u' : Fin m → ℝ) (xStar' : Fin n → ℝ) => ↑(K u' xStar')) u xStar = ↑(K u xStar)

Helper for Corollary33.3.3: the EReal simple extensions of a real kernel are globally ordered, and on C × D they both reduce to the original real kernel after coercion.

structure SaddleClosednessPredicates {m n : ℕ} (K : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Type

• lowerClosed : Prop
• upperClosed : Prop

def saddleClosednessPredicates {m n : ℕ} (K : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : SaddleClosednessPredicates K

@[reducible]

def IsLowerClosedSaddleFunction {m n : ℕ} : ((Fin m → ℝ) → (Fin n → ℝ) → EReal) → Prop

@[reducible]

def IsUpperClosedSaddleFunction {m n : ℕ} : ((Fin m → ℝ) → (Fin n → ℝ) → EReal) → Prop

theorem helperForCorollary33_3_3_closurePair_implies_closedness_and_order {m n : ℕ} {K1 K2 : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK1 : IsConcaveConvexOn Set.univ Set.univ K1) (hK2 : IsConcaveConvexOn Set.univ Set.univ K2) (hPair : K2 = concaveClosureInFirst K1 ∧ convexClosureInSecond K2 = K1) : IsLowerClosedSaddleFunction K1 ∧ IsUpperClosedSaddleFunction K2 ∧ ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), K1 u xStar ≤ K2 u xStar

Helper for Corollary33.3.3: once the lower and upper simple extensions are identified as the expected coordinatewise closure pair, their lower-closedness, upper-closedness, and pointwise order follow formally from the Section 33 closure machinery already available in this split file.

def erealOfRealBifunction {m n : ℕ} : ((Fin m → ℝ) → (Fin n → ℝ) → ℝ) → (Fin m → ℝ) → (Fin n → ℝ) → EReal

@[reducible]

noncomputable def lowerSimpleExtensionOfReal {m n : ℕ} : Set (Fin m → ℝ) → Set (Fin n → ℝ) → ((Fin m → ℝ) → (Fin n → ℝ) → ℝ) → (Fin m → ℝ) → (Fin n → ℝ) → EReal

@[reducible]

noncomputable def upperSimpleExtensionOfReal {m n : ℕ} : Set (Fin m → ℝ) → Set (Fin n → ℝ) → ((Fin m → ℝ) → (Fin n → ℝ) → ℝ) → (Fin m → ℝ) → (Fin n → ℝ) → EReal

theorem helperForCorollary33_3_3_lowerSimpleExtensionOfReal_nonbotSlice_set_eq {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hD_nonempty : D.Nonempty) : {u : Fin m → ℝ | ∃ (xStar : Fin n → ℝ), lowerSimpleExtensionOfReal C D K u xStar ≠ ⊥} = C

Helper for Corollary33.3.3: the lower simple extension of a real-valued kernel has exactly the original primal constraint set as the locus where some value is not ⊥.

theorem helperForCorollary33_3_3_upperSimpleExtensionOfReal_nontopSlice_set_eq {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_nonempty : C.Nonempty) : {xStar : Fin n → ℝ | ∃ (u : Fin m → ℝ), upperSimpleExtensionOfReal C D K u xStar ≠ ⊤} = D

Helper for Corollary33.3.3: the upper simple extension of a real-valued kernel has exactly the original dual constraint set as the locus where some value is not ⊤.

theorem helperForCorollary33_3_3_simpleExtension_sliceDomains_eq_constraints {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_nonempty : C.Nonempty) (hD_nonempty : D.Nonempty) : {u : Fin m → ℝ | ∃ (xStar : Fin n → ℝ), lowerSimpleExtensionOfReal C D K u xStar ≠ ⊥} = C ∧ {xStar : Fin n → ℝ | ∃ (u : Fin m → ℝ), upperSimpleExtensionOfReal C D K u xStar ≠ ⊤} = D

Helper for Corollary33.3.3: the two real-valued simple extensions recover exactly the original primal and dual constraint sets as their non-infinite slice domains.

theorem helperForCorollary33_3_3_upperSimpleExtensionOfReal_offParameterSection {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {u : Fin m → ℝ} (hu : u ∉ C) : upperSimpleExtensionOfReal C D K u = fun (xStar : Fin n → ℝ) => if xStar ∈ D then ⊥ else ⊤

Helper for Corollary33.3.3: outside the primal constraint set C, the upper simple extension freezes to the top/bottom indicator of the dual constraint set D.

theorem helperForCorollary33_3_3_upperSimpleExtensionOfReal_offParameterSection_mixedValues {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {u : Fin m → ℝ} (hu : u ∉ C) {xIn xOut : Fin n → ℝ} (hxIn : xIn ∈ D) (hxOut : xOut ∉ D) : upperSimpleExtensionOfReal C D K u xIn = ⊥ ∧ upperSimpleExtensionOfReal C D K u xOut = ⊤

Helper for Corollary33.3.3: an off-C section of the upper simple extension attains ⊥ on D and ⊤ off D.

theorem helperForCorollary33_3_3_upperSimpleExtensionOfReal_onDualSection_not_convexOn_univ {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {xStar : Fin n → ℝ} (hxStar : xStar ∈ D) {uIn uOut : Fin m → ℝ} (_huIn : uIn ∈ C) (huOut : uOut ∉ C) (hMidIn : (1 / 2) • uIn + (1 / 2) • uOut ∈ C) : ¬IsERealConvexOn Set.univ fun (u : Fin m → ℝ) => upperSimpleExtensionOfReal C D K u xStar

Helper for Corollary33.3.3: if one primal point lies in C, another lies outside C, and their midpoint returns to C, then freezing the upper simple extension at a dual point of D produces a first-variable section that is not convex on all of ℝ^m.

theorem helperForCorollary33_3_3_upperSimpleExtensionOfReal_not_convexConcaveOn_univ_of_midpoint_witness {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {xStar : Fin n → ℝ} (hxStar : xStar ∈ D) {uIn uOut : Fin m → ℝ} (huIn : uIn ∈ C) (huOut : uOut ∉ C) (hMidIn : (1 / 2) • uIn + (1 / 2) • uOut ∈ C) : ¬IsConvexConcaveOn Set.univ Set.univ (upperSimpleExtensionOfReal C D K)

Helper for Corollary33.3.3: the midpoint witness above already rules out the convex-concave orientation for the upper simple extension on all of ℝ^m × ℝ^n.

theorem helperForCorollary33_3_3_upperSimpleExtensionOfReal_convexConcaveUpperClosedBranch_impossible_of_midpoint_witness {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {xStar : Fin n → ℝ} (hxStar : xStar ∈ D) {uIn uOut : Fin m → ℝ} (huIn : uIn ∈ C) (huOut : uOut ∉ C) (hMidIn : (1 / 2) • uIn + (1 / 2) • uOut ∈ C) : ¬(IsConvexConcaveOn Set.univ Set.univ (upperSimpleExtensionOfReal C D K) ∧ concaveClosureInSecond (convexClosureInFirst (upperSimpleExtensionOfReal C D K)) = upperSimpleExtensionOfReal C D K)

Helper for Corollary33.3.3: once the midpoint witness rules out the global convex-concave orientation of the upper simple extension, the right-hand branch in the definition of IsUpperClosedSaddleFunction is impossible as well.

theorem helperForCorollary33_3_3_not_upperClosed_of_branch_obstructions {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hLeft : ¬(IsConcaveConvexOn Set.univ Set.univ K ∧ concaveClosureInFirst (convexClosureInSecond K) = K)) (hRight : ¬(IsConvexConcaveOn Set.univ Set.univ K ∧ concaveClosureInSecond (convexClosureInFirst K) = K)) : ¬IsUpperClosedSaddleFunction K

Helper for Corollary33.3.3: any proof of upper closedness must choose one of the two closure branches, so refuting both branches separately refutes upper closedness itself.

@[reducible]

noncomputable def helperForCorollary33_3_3_canonicalWitness {m n : ℕ} (C : Set (Fin m → ℝ)) (D : Set (Fin n → ℝ)) (K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

Helper for Corollary33.3.3: the canonical witness is obtained by taking the sectionwise convex conjugate of the lower simple extension.

theorem helperForCorollary33_3_3_canonicalWitness_primalFormula {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (u : Fin m → ℝ) (x : Fin n → ℝ) : helperForCorollary33_3_3_canonicalWitness C D K u x = if x_1 : u ∈ C then sSup (Set.range fun (xStar : ↑D) => ↑(x ⬝ᵥ ↑xStar - K u ↑xStar)) else ⊤

Helper for Corollary33.3.3: the canonical witness has the textbook primal supremum formula.

theorem helperForCorollary33_3_3_canonicalWitness_offParameterSection {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {u : Fin m → ℝ} (hu : u ∉ C) : helperForCorollary33_3_3_canonicalWitness C D K u = fun (x : Fin n → ℝ) => ⊤

Helper for Corollary33.3.3: outside the primal constraint set C, the canonical witness section is constantly ⊤.

theorem helperForCorollary33_3_3_canonicalWitness_hasNoBotValues {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hD_nonempty : D.Nonempty) : HasNoBotValuesBifunction (helperForCorollary33_3_3_canonicalWitness C D K)

Helper for Corollary33.3.3: the canonical witness never takes the value ⊥.