theorem
proved
tactic proof
excluded_middle_implies_continuous
show as:
view Lean formalization →
formal statement (Lean)
214theorem excluded_middle_implies_continuous
215 (C : ComparisonOperator)
216 (hEM : ExcludedMiddle C) :
217 ContinuousOn (derivedCost C) (Set.Ioi 0) := by
proof body
Tactic-mode proof.
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
245/-- **Translation lemma 4 (Route-independence ⇒ Multiplicative consistency
246with a symmetric polynomial combiner)**: extracted directly from the
247definition of `RouteIndependence`. -/