isSemiconjugacy_id_iff_eq — Mathlib

English

The identity map is a semiconjugacy from ϕ to ψ if and only if ϕ and ψ are equal.

Русский

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

LaTeX

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

Lean4

/-- The identity is a semiconjugacy from `ϕ` to `ψ` if and only if `ϕ` and `ψ` are equal. -/
theorem isSemiconjugacy_id_iff_eq (ϕ ψ : Flow τ α) : IsSemiconjugacy id ϕ ψ ↔ ϕ = ψ :=
  ⟨fun h => ext h.semiconj, fun h => h.recOn ⟨continuous_id, surjective_id, fun _ => .id_left⟩⟩

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