English
If there exists z with z ∈ ball x(dynEntourage(T,U,n)) and z ∈ ball y(dynEntourage(T,U,n)), then x ∈ ball y(dynEntourage(T, U∘U, n)).
Русский
Если существует z such, что z находится как в шаре вокруг x радиону dynEntourage(T,U,n), так и в шаре вокруг y, то x внутри шара вокруг y для окружения dynEntourage(T, U∘U, n).
LaTeX
$$$\text{If } (\mathrm{ball}\,x(\mathrm{dynEntourage}(T,U,n)) \cap \mathrm{ball}\,y(\mathrm{dynEntourage}(T,U,n))) \neq \emptyset, \text{ then } x \in \mathrm{ball}\,y(\mathrm{dynEntourage}(T,U\circ U,n)).$$$
Lean4
theorem mem_ball_dynEntourage_comp (T : X → X) (n : ℕ) {U : Set (X × X)} (U_symm : IsSymmetricRel U) (x y : X)
(h : (ball x (dynEntourage T U n) ∩ ball y (dynEntourage T U n)).Nonempty) :
x ∈ ball y (dynEntourage T (U ○ U) n) := by
rcases h with ⟨z, z_Bx, z_By⟩
rw [mem_ball_symmetry (IsSymmetricRel.dynEntourage T U_symm n)] at z_Bx
exact dynEntourage_comp_subset T U U n (mem_ball_comp z_By z_Bx)
