dynEntourage_zero — Mathlib

English

For any T and U, the dynamical entourage at time 0 is the universal relation: dynEntourage(T, U, 0) = univ.

Русский

Для любого T и U динамическое окружение в момент времени 0 равно всеобщему отношению: dynEntourage(T, U, 0) = univ.

LaTeX

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

Lean4

@[simp]
theorem dynEntourage_zero {T : X → X} {U : Set (X × X)} : dynEntourage T U 0 = univ := by simp [dynEntourage]

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