mem_ball_dynEntourage — Mathlib

English

A point y lies in the ball around x with radius dynEntourage(T,U,n) if and only if for all k < n, T^k y lies in the ball around T^k x with respect to U.

Русский

Точка y принадлежит шар вокруг x радиуса dynEntourage(T,U,n) тогда и только тогда, когда для всех k < n T^k y лежит в шаре вокруг T^k x по U.

LaTeX

$$$y \in \mathrm{ball}(x, \mathrm{dynEntourage}(T,U,n)) \iff \forall k < n, T^{k}y \in \mathrm{ball}(T^{k}x, U)$$$

Lean4

theorem mem_ball_dynEntourage {T : X → X} {U : Set (X × X)} {n : ℕ} {x y : X} :
    y ∈ ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ ball (T^[k] x) U := by
  simp only [ball, mem_preimage, mem_dynEntourage]

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