dynEntourage_one — Mathlib

English

For any map T and entourage U, the dynamical entourage at time 1 is exactly U: dynEntourage(T, U, 1) = U.

Русский

Для любой функции T и окутывания U динамическое окутывание в момент времени 1 совпадает с U: dynEntourage(T, U, 1) = U.

LaTeX

$$$\mathrm{dynEntourage}(T,U,1) = U.$$$

Lean4

@[simp]
theorem dynEntourage_one {T : X → X} {U : Set (X × X)} : dynEntourage T U 1 = U := by simp [dynEntourage]

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