self

Mathlib.Dynamics.Flow

URI: https://scilib.ai/kg/mathlib#Flow.IsFactorOf.self

English

The identity is a semiconjugacy from ϕ to ψ if and only if ϕ = ψ.

Русский

Идентичность является полусопряжением от ϕ к ψ тогда и только тогда, когда ϕ = ψ.

LaTeX

$$$IsFactorOf(\\\\mathrm{id}, ϕ, ψ) \\iff ϕ = ψ.$$$

Lean4

/-- Every flow is a factor of itself. -/
theorem self : IsFactorOf ϕ ϕ :=
  ⟨id, (isSemiconjugacy_id_iff_eq ϕ ϕ).mpr (by rfl)⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru