ext — Mathlib

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 _ _

Похожие утверждения