dynEntourage_eq_inter_Ico — Mathlib

English

The n-th dynamical entourage can also be expressed as the intersection over k in the half-open interval Ico(0,n) of the preimage under (map T T)^k of U.

Русский

n-й динамический окрестности можно выразить как пересечение по k в Ico(0,n) предобраза от (map T T)^k(U).

LaTeX

$$$\operatorname{dynEntourage}(T,U,n) = \bigcap_{k \in \mathrm{Ico}(0,n)} ( (\operatorname{map} T T)^{k} )^{-1}(U)$$$

Lean4

theorem dynEntourage_eq_inter_Ico (T : X → X) (U : Set (X × X)) (n : ℕ) :
    dynEntourage T U n = ⋂ k : Ico 0 n, (map T T)^[k] ⁻¹' U := by simp [dynEntourage]

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