mono — Mathlib

English

If γ is an integral curve on a set s for the vector field v, then γ is an integral curve on any subset s′ of s.

Русский

Пусть γ является интегральной кривой векторного поля v на области s; тогда γ является интегральной кривой на любой подмножине s′ ⊆ s.

LaTeX

$$$\mathrm{IsMIntegralCurveOn}(\gamma,v,s) \;\wedge\; s' \subseteq s \;\Rightarrow\; \mathrm{IsMIntegralCurveOn}(\gamma,v,s').$$$

Lean4

theorem mono (h : IsMIntegralCurveOn γ v s) (hs : s' ⊆ s) : IsMIntegralCurveOn γ v s' := fun t ht ↦
  (h t (hs ht)).mono hs

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