Theorems · Inductive type · dynamical systems

Flow.IsSemiconjugacy

{τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddMonoid τ] → {β : Type u_3} → [inst_3 : TopologicalSpace β] → (α → β) → Flow τ α → Flow τ β → Prop

Given flows ϕ by τ on α and ψ by τ on β, a function π : α → β is called a semiconjugacy from ϕ to ψ if π is continuous and surjective, and π ∘ (ϕ t) = (ψ t) ∘ π for all t : τ.

Defined in

Mathlib.Dynamics.Flow

Cited by

7 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceAddMonoidTopologicalSpace