English
Two flows that agree at all times and states are equal.
Русский
Два потока, совпадающих при всех значениях времени и состояний, равны.
LaTeX
$$$\forall ϕ_1\, ϕ_2,\ (\forall t \forall x,\ ϕ_1(t)(x) = ϕ_2(t)(x)) \Rightarrow ϕ_1 = ϕ_2$$$
Lean4
@[ext]
theorem ext : ∀ {ϕ₁ ϕ₂ : Flow τ α}, (∀ t x, ϕ₁ t x = ϕ₂ t x) → ϕ₁ = ϕ₂
| ⟨f₁, _, _, _⟩, ⟨f₂, _, _, _⟩, h => by
congr
funext
exact h _ _