Theorems · Definition · dynamical systems

Flow.toFun

{τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddZero τ] → Flow τ α → τ → α → α

The map τ → α → α underlying a flow of τ on α.

Defined in

Mathlib.Dynamics.Flow

Cited by

34 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceAddZero