English
In a boundaryless manifold, equality on an Ioo interval follows from contMDiff and integral-curve hypotheses.
Русский
На границах без границ равенство на интервале Ioo следует из contMDiff и гипотез об интегральной кривой.
LaTeX
$$$\text{Boundaryless}(I,M) \Rightarrow (isMIntegralCurveOn_Ioo_eqOn_of_contMDiff)$.$$
Lean4
/-- Integral curves are unique on open intervals.
If a $C^1$ vector field `v` admits two integral curves `γ γ' : ℝ → M` on some open interval
`Ioo a b`, and `γ t₀ = γ' t₀` for some `t ∈ Ioo a b`, then `γ` and `γ'` agree on `Ioo a b`. -/
theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff (ht₀ : t₀ ∈ Ioo a b) (hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t))
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (hγ : IsMIntegralCurveOn γ v (Ioo a b))
(hγ' : IsMIntegralCurveOn γ' v (Ioo a b)) (h : γ t₀ = γ' t₀) : EqOn γ γ' (Ioo a b) :=
by
set s := {t | γ t = γ' t} ∩ Ioo a b with hs
suffices hsub : Ioo a b ⊆ s from fun t ht ↦ mem_setOf.mp ((subset_def ▸ hsub) t ht).1
apply isPreconnected_Ioo.subset_of_closure_inter_subset (s := Ioo a b) (u := s) _ ⟨t₀, ⟨ht₀, ⟨h, ht₀⟩⟩⟩
· -- is this really the most convenient way to pass to subtype topology?
-- TODO: shorten this when better API around subtype topology exists
rw [hs, inter_comm, ← Subtype.image_preimage_val, inter_comm, ← Subtype.image_preimage_val,
image_subset_image_iff Subtype.val_injective, preimage_setOf_eq]
intro t ht
rw [mem_preimage, ← closure_subtype] at ht
revert ht t
apply IsClosed.closure_subset (isClosed_eq _ _)
· rw [continuous_iff_continuousAt]
rintro ⟨_, ht⟩
apply ContinuousAt.comp _ continuousAt_subtype_val
rw [Subtype.coe_mk]
exact hγ.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)
· rw [continuous_iff_continuousAt]
rintro ⟨_, ht⟩
apply ContinuousAt.comp _ continuousAt_subtype_val
rw [Subtype.coe_mk]
exact hγ'.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)
· rw [isOpen_iff_mem_nhds]
intro t₁ ht₁
have hmem := Ioo_mem_nhds ht₁.2.1 ht₁.2.2
have heq : γ =ᶠ[𝓝 t₁] γ' :=
isMIntegralCurveAt_eventuallyEq_of_contMDiffAt (hγt _ ht₁.2) hv.contMDiffAt (hγ.isMIntegralCurveAt hmem)
(hγ'.isMIntegralCurveAt hmem) ht₁.1
apply (heq.and hmem).mono
exact fun _ ht ↦ ht
