polynomial_continuous

formal source

 274any polynomial of total degree at most two on `ℝ × ℝ` is continuous, so
 275`SatisfiesLawsOfLogic ⊆ SatisfiesLawsOfLogicContinuous`. -/
 276
 277private theorem polynomial_continuous
 278    (a b c d e f : ℝ) :
 279    Continuous (Function.uncurry
 280      (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2)) := by
 281  unfold Function.uncurry
 282  fun_prop
 283
 284/-- Polynomial route-independence implies continuous route-independence. -/
 285theorem polynomial_implies_continuous (C : ComparisonOperator)
 286    (hPoly : RouteIndependence C) :
 287    ContinuousRouteIndependence C := by
 288  obtain ⟨P, ⟨a, b, c, d, e, f, hPform⟩, hSymP, hCons⟩ := hPoly
 289  refine ⟨P, ?_, hSymP, hCons⟩
 290  -- Continuity of P from its polynomial form.
 291  have heq : Function.uncurry P
 292      = Function.uncurry (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2) := by
 293    funext ⟨u, v⟩
 294    simpa using hPform u v
 295  rw [heq]
 296  exact polynomial_continuous a b c d e f
 297
 298/-- The polynomial-case `SatisfiesLawsOfLogic` is a special case of the
 299continuous-case `SatisfiesLawsOfLogicContinuous`. -/
 300theorem laws_polynomial_implies_continuous
 301    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 302    SatisfiesLawsOfLogicContinuous C where
 303  identity := h.identity
 304  non_contradiction := h.non_contradiction
 305  excluded_middle := h.excluded_middle
 306  scale_invariant := h.scale_invariant
 307  route_independence := polynomial_implies_continuous C h.route_independence