dynEntourage — Mathlib

English

If U is open in X × X and T is continuous, then for every n the dynamical entourage dynEntourage(T,U,n) is open.

Русский

Если U открыто в X×X и T непрерывно, то для каждого n динамическое окрестность dynEntourage(T,U,n) открыта.

LaTeX

$$$\text{IsOpen}(\operatorname{dynEntourage}(T,U,n))$ for all n, given U открыто и T непрерывно.$$

Lean4

theorem _root_.isOpen.dynEntourage [TopologicalSpace X] {T : X → X} (T_cont : Continuous T) {U : Set (X × X)}
    (U_open : IsOpen U) (n : ℕ) : IsOpen (dynEntourage T U n) :=
  by
  rw [dynEntourage_eq_inter_Ico T U n]
  refine isOpen_iInter_of_finite fun k ↦ ?_
  exact U_open.preimage ((T_cont.prodMap T_cont).iterate k)

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