chore(Dynamics): factor out a definition and fix names (leanprover-community#37402)

Define the identity as a constant flow and correct a few names.

Author: mcdoll

Mathlib/Dynamics/Flow.lean

@@ -105,14 +105,22 @@ namespace Flow
 variable {τ : Type*} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ]
   {α : Type*} [TopologicalSpace α] (ϕ : Flow τ α)
 
-instance : Inhabited (Flow τ α) :=
-  ⟨{  toFun := fun _ x => x
-      cont' := continuous_snd
-      map_add' := fun _ _ _ => rfl
-      map_zero' := fun _ => rfl }⟩
-
 instance : CoeFun (Flow τ α) fun _ => τ → α → α := ⟨Flow.toFun⟩
 
+variable (τ α) in
+/-- The identity map as a constant flow. -/
+protected def id : Flow τ α where
+  toFun _ := id
+  cont' := continuous_snd
+  map_add' _ _ _ := rfl
+  map_zero' _ := rfl
+
+@[simp]
+theorem id_apply (t : τ) : Flow.id τ α t = id := rfl
+
+instance : Inhabited (Flow τ α) :=
+  ⟨Flow.id τ α⟩
+
 @[ext]
 theorem ext : ∀ {ϕ₁ ϕ₂ : Flow τ α}, (∀ t x, ϕ₁ t x = ϕ₂ t x) → ϕ₁ = ϕ₂
   | ⟨f₁, _, _, _⟩, ⟨f₂, _, _, _⟩, h => by

Mathlib/Dynamics/OmegaLimit.lean

@@ -134,11 +134,14 @@ theorem mem_omegaLimit_iff_frequently₂ (y : β) :
 
 /-- An element `y` is in the ω-limit of `x` w.r.t. `f` if the forward
 images of `x` frequently (w.r.t. `f`) falls within an arbitrary neighbourhood of `y`. -/
-theorem mem_omegaLimit_singleton_iff_map_cluster_point (x : α) (y : β) :
+theorem mem_omegaLimit_singleton_iff_mapClusterPt (x : α) (y : β) :
     y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t ↦ ϕ t x := by
   simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff_frequently, singleton_inter_nonempty,
     mem_preimage]
 
+@[deprecated (since := "2026-03-31")]
+alias mem_omegaLimit_singleton_iff_map_cluster_point := mem_omegaLimit_singleton_iff_mapClusterPt
+
 /-!
 ### Set operations and omega limits
 -/
@@ -187,13 +190,16 @@ theorem omegaLimit_eq_iInter_inter {v : Set τ} (hv : v ∈ f) :
   rw [omegaLimit_eq_biInter_inter _ _ _ hv]
   apply biInter_eq_iInter
 
-theorem omegaLimit_subset_closure_fw_image {u : Set τ} (hu : u ∈ f) :
+theorem omegaLimit_subset_closure_image2 {u : Set τ} (hu : u ∈ f) :
     ω f ϕ s ⊆ closure (image2 ϕ u s) := by
   rw [omegaLimit_eq_iInter]
   intro _ hx
   rw [mem_iInter] at hx
   exact hx ⟨u, hu⟩
 
+@[deprecated (since := "2026-03-31")]
+alias omegaLimit_subset_closure_fw_image := omegaLimit_subset_closure_image2
+
 -- An instance with better keys
 instance : Inhabited f.sets := Filter.inhabitedMem
 
@@ -348,7 +354,7 @@ theorem omegaLimit_omegaLimit (hf : ∀ t, Tendsto (t + ·) f f) : ω f ϕ (ω f
       (inter_subset_inter_left _
         ((isInvariant_iff_image _ _).mp (isInvariant_omegaLimit _ _ _ hf) _))
   have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
-    l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_fw_image _ _ _ hu hb.1, hb.2⟩
+    l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_image2 _ _ _ hu hb.1, hb.2⟩
   have l₃ : (o ∩ image2 ϕ u s).Nonempty := by
     rcases l₂ with ⟨b, hb₁, hb₂⟩
     exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)