diagonal_continuous_on_range

formal source

  82
  83/-- **The diagonal of Φ on Range(F) is continuous.**  Pure consequence of
  84joint continuity of Φ on Range(F)². -/
  85theorem diagonal_continuous_on_range
  86    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
  87    (hClosed : IteratedClosureOnRange F Phi) :
  88    ContinuousOn (fun v : ℝ => Phi v v) (Set.image F (Set.Ioi 0)) := by
  89  obtain ⟨hCont, _⟩ := hClosed
  90  -- The diagonal map v ↦ (v, v) is continuous everywhere; compose with Phi.
  91  have h_diag_on : ContinuousOn (fun w : ℝ => ((w, w) : ℝ × ℝ))
  92      (Set.image F (Set.Ioi 0)) :=
  93    (continuous_id.prodMk continuous_id).continuousOn
  94  have h_maps : Set.MapsTo (fun w : ℝ => ((w, w) : ℝ × ℝ))
  95      (Set.image F (Set.Ioi 0))
  96      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
  97    intro w hw
  98    exact ⟨hw, hw⟩
  99  -- Use ContinuousOn.comp on the explicit lambda form of uncurry.
 100  have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
 101      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont
 102  have h_comp : ContinuousOn
 103      ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
 104      (Set.image F (Set.Ioi 0)) :=
 105    h_phi_on.comp h_diag_on h_maps
 106  -- Convert the composition into the simpler form.
 107  have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
 108              = (fun v : ℝ => Phi v v) := by
 109    funext w
 110    rfl
 111  rw [h_eq] at h_comp
 112  exact h_comp
 113
 114/-- **Iteration produces continuous orbits.**  If we iterate Φ on a starting
 115element v ∈ Range(F), the n-fold iterate is again in Range(F), and the map