English
For a sequence u: ℕ → α in a complete lattice and any natural number n, the supremum of the tail starting at n is the same as the supremum of the sequence shifted by n: ⨆ i ≥ n, u(i) = ⨆ i, u(i + n).
Русский
Для последовательности u: ℕ → α в полной решетке и любого натурального числа n верхняя грань хвоста, начиная с n, равна верхней грани сдвинутой последовательности: ⨆ i ≥ n, u(i) = ⨆ i, u(i + n).
LaTeX
$$$\big\lVert \big\lVert i \ge n \; u(i) \big\rVert \big\rVert = \big\lVert i \in \mathbb{N} \; u(i+n) \big\lVert$$$
Lean4
theorem iSup_ge_eq_iSup_nat_add (u : ℕ → α) (n : ℕ) : ⨆ i ≥ n, u i = ⨆ i, u (i + n) :=
by
apply le_antisymm <;> simp only [iSup_le_iff]
· refine fun i hi => le_sSup ⟨i - n, ?_⟩
dsimp only
rw [Nat.sub_add_cancel hi]
· exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩
