trans

Mathlib.Dynamics.Flow

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

← MathLib Explorer

English

Every flow is a factor of itself.

Русский

Каждый поток является фактором самого себя.

LaTeX

$$$IsFactorOf\\\\ ϕ \\\\ ϕ.$$$

Lean4

/-- Transitivity of factors of flows. -/
theorem trans (h₁ : IsFactorOf ϕ ψ) (h₂ : IsFactorOf ψ χ) : IsFactorOf ϕ χ :=
  h₁.elim fun π hπ => h₂.elim fun ρ hρ => ⟨π ∘ ρ, hρ.comp χ ψ ϕ hπ⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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