isFactorOf

Mathlib.Dynamics.Flow

URI: https://scilib.ai/kg/mathlib#Flow.IsSemiconjugacy.isFactorOf

English

If ϕ is a factor of ψ and ψ is a factor of χ, then ϕ is a factor of χ.

Русский

Если ϕ является фактором ψ, а ψ является фактором χ, то ϕ является фактором χ.

LaTeX

$$$IsFactorOf\\\\ ϕ χ \\;\\;\\text{при условии } IsFactorOf\\\\ ϕ ψ, IsFactorOf\\\\ ψ χ.$$$

Lean4

theorem isFactorOf {π : α → β} (h : IsSemiconjugacy π ϕ ψ) : IsFactorOf ψ ϕ :=
  ⟨π, h⟩

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

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

Разделы

Аффилиация

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