English
The composition of two dynamical entourages is contained in the dynamical entourage of the composed relation: (dynEntourage T U n) ∘ (dynEntourage T V n) ⊆ dynEntourage T (U ○ V) n.
Русский
Произведение двух динамических окрестностей содержится в динамической окрестности для композиции: (dynEntourage T U n) ∘ (dynEntourage T V n) ⊆ dynEntourage T (U ○ V) n.
LaTeX
$$$\bigl(dynEntourage(T,U,n)\bigr) \circ \bigl(dynEntourage(T,V,n)\bigr) \subseteq dynEntourage(T, U \circ V, n).$$$
Lean4
theorem dynEntourage_comp_subset (T : X → X) (U V : Set (X × X)) (n : ℕ) :
(dynEntourage T U n) ○ (dynEntourage T V n) ⊆ dynEntourage T (U ○ V) n :=
by
simp only [dynEntourage, map_iterate, subset_iInter_iff]
intro k k_n xy xy_comp
simp only [compRel, mem_iInter, mem_preimage, map_apply, mem_setOf_eq] at xy_comp ⊢
rcases xy_comp with ⟨z, hz1, hz2⟩
exact mem_ball_comp (hz1 k k_n) (hz2 k k_n)
