iInf_ge_eq_iInf_nat_add — Mathlib

English

For a sequence u: ℕ → α in a complete lattice and n ∈ ℕ, the infimum over i ≥ n of u(i) equals the infimum over i of u(i + n): ⨅ i ≥ n, u(i) = ⨅ i, u(i + n).

Русский

Для последовательности u: ℕ → α в полной решетке и n ∈ ℕ, инфиминум по i ≥ n от u(i) равен инфиминуму по i от u(i+n).

LaTeX

$$$\inf_{i \ge n} u(i) = \inf_{i \in \mathbb{N}} u(i+n)$$$

Lean4

theorem iInf_ge_eq_iInf_nat_add (u : ℕ → α) (n : ℕ) : ⨅ i ≥ n, u i = ⨅ i, u (i + n) :=
  @iSup_ge_eq_iSup_nat_add αᵒᵈ _ _ _

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