uniformity_basis_dist_pow_of_lt_one

English

If u is a sequence of real numbers and c≥0, and c·u(k) ≤ u(k+1) for k < n, then c^n u(0) ≤ u(n).

Русский

Если u — последовательность вещественных чисел и c≥0, и для всех k<n выполняется c·u(k) ≤ u(k+1), то c^n u(0) ≤ u(n).

LaTeX

$$$$ c^n \\cdot u(0) \\le u(n) \\quad \\text{for all } n, \\text{ given } c\\ge 0 \\text{ and } u(k+1) \\ge c\\cdot u(k). $$$$

Lean4

theorem uniformity_basis_dist_pow_of_lt_one {α : Type*} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) :
    (uniformity α).HasBasis (fun _ : ℕ ↦ True) fun k ↦ {p : α × α | dist p.1 p.2 < r ^ k} :=
  Metric.mk_uniformity_basis (fun _ _ ↦ pow_pos h₀ _) fun _ ε0 ↦
    (exists_pow_lt_of_lt_one ε0 h₁).imp fun _ hk ↦ ⟨trivial, hk.le⟩

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