eq_zero_of_mem_fdo_of_T_zpow_mem_fdo

English

If z ∈ 𝒟ᵒ and T^n • z ∈ 𝒟ᵒ, then n = 0.

Русский

Если z ∈ 𝒟ᵒ и T^n • z ∈ 𝒟ᵒ, тогда n = 0.

LaTeX

$$$\forall z\in 𝒟^{\circ}, \forall n\in \mathbb{Z},\; T^{n} \cdot z \in 𝒟^{\circ} \Rightarrow n = 0$$$

Lean4

theorem eq_zero_of_mem_fdo_of_T_zpow_mem_fdo {n : ℤ} (hz : z ∈ 𝒟ᵒ) (hg : T ^ n • z ∈ 𝒟ᵒ) : n = 0 :=
  by
  suffices |(n : ℝ)| < 1 by rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
  have h₁ := hz.2
  have h₂ := hg.2
  rw [re_T_zpow_smul] at h₂
  calc
    |(n : ℝ)| ≤ |z.re| + |z.re + (n : ℝ)| := abs_add' (n : ℝ) z.re
    _ < 1 / 2 + 1 / 2 := (add_lt_add h₁ h₂)
    _ = 1 := add_halves 1

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