comp — Mathlib

English

If π semiconjugates ϕ to ψ and ρ semiconjugates ψ to χ, then ρ ∘ π semiconjugates ϕ to χ.

Русский

Если π полусопряжает ϕ к ψ, а ρ полусопрягaет ψ к χ, то ρ ∘ π полусопряжает ϕ к χ.

LaTeX

$$$IsSemiconjugacy(ρ \\circ π, ϕ, χ).$$$

Lean4

/-- The composition of semiconjugacies is a semiconjugacy. -/
theorem comp {π : α → β} {ρ : β → γ} (h₁ : IsSemiconjugacy π ϕ ψ) (h₂ : IsSemiconjugacy ρ ψ χ) :
    IsSemiconjugacy (ρ ∘ π) ϕ χ :=
  ⟨h₂.cont.comp h₁.cont, h₂.surj.comp h₁.surj, fun t => (h₂.semiconj t).comp_left (h₁.semiconj t)⟩

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