dynEntourage_univ — Mathlib

English

For any T, the dynamical entourage with the universal entourage is universal for all n: dynEntourage(T, univ, n) = univ.

Русский

Для любой функции T динамическое окутывание с универсальным окружением равно универсальному для любого n: dynEntourage(T, univ, n) = univ.

LaTeX

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

Lean4

@[simp]
theorem dynEntourage_univ {T : X → X} {n : ℕ} : dynEntourage T univ n = univ := by simp [dynEntourage]

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