restrictNonneg — Mathlib

English

Restrict a flow ϕ to the additive submonoid of nonnegative elements of τ, obtaining a flow on α with time domain AddSubmonoid.nonneg τ.

Русский

Ограничиваем поток ϕ до подгруппы неотрицательных элементов τ, получая поток на α с временем из AddSubmonoid.nonneg τ.

LaTeX

$$$\\text{restrictNonneg} : \\text{Flow}(\\text{AddSubmonoid.nonneg}\\, \\tau)\\; \\alpha \\;\\text{в }\\alpha.$$$

Lean4

/-- Restrict a flow by `τ` to a flow by the additive submonoid of nonnegative elements of `τ`. -/
def restrictNonneg : Flow (AddSubmonoid.nonneg τ) α :=
  ϕ.restrictAddSubmonoid (.nonneg τ)

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