IsFactorOf — Mathlib

English

A flow ψ is called a factor of ϕ if there exists a semiconjugacy π from ϕ to ψ.

Русский

Поток ψ называется фактором ϕ, если существует полусопряжение π от ϕ к ψ.

LaTeX

$$$\\exists \\pi: \\alpha \\to \\beta,\\ IsSemiconjugacy(\\pi, ϕ, ψ).$$$

Lean4

/-- A flow `ψ` is called a *factor* of `ϕ` if there exists a semiconjugacy from `ϕ` to `ψ`. -/
def IsFactorOf (ψ : Flow τ β) (ϕ : Flow τ α) : Prop :=
  ∃ π : α → β, IsSemiconjugacy π ϕ ψ

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