excluded_middle_implies_continuous

formal source

 211continuous everywhere; the uncurried C is continuous on the positive
 212quadrant by ExcludedMiddle. The pair-map sends (0, ∞) into the positive
 213quadrant. Hence the composition is continuous on (0, ∞). -/
 214theorem excluded_middle_implies_continuous
 215    (C : ComparisonOperator)
 216    (hEM : ExcludedMiddle C) :
 217    ContinuousOn (derivedCost C) (Set.Ioi 0) := by
 218  -- Pair-map r ↦ (r, 1) is continuous everywhere.
 219  have h_pair_cont : Continuous (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ)) :=
 220    continuous_id.prodMk continuous_const
 221  have h_pair_on : ContinuousOn (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
 222      (Set.Ioi (0 : ℝ)) :=
 223    h_pair_cont.continuousOn
 224  -- Pair-map sends (0,∞) into the positive quadrant.
 225  have h_maps : Set.MapsTo (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
 226      (Set.Ioi (0 : ℝ)) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)) := by
 227    intro s hs
 228    refine ⟨?_, ?_⟩
 229    · exact hs
 230    · show (0 : ℝ) < 1
 231      exact one_pos
 232  -- Compose to get continuity of (uncurry C) ∘ pair on (0,∞).
 233  have h_comp : ContinuousOn
 234      ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
 235      (Set.Ioi (0 : ℝ)) :=
 236    hEM.comp h_pair_on h_maps
 237  -- The composition equals derivedCost C definitionally.
 238  have h_eq : ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
 239              = derivedCost C := by
 240    funext s
 241    rfl
 242  rw [h_eq] at h_comp
 243  exact h_comp
 244