mk_le_of_forall_le — Mathlib

English

If a tail of a Cauchy sequence f is bounded above by x, then mk(f) ≤ x.

Русский

Если хвост последовательности f ограничен сверху числом x, то mk(f) ≤ x.

LaTeX

$$$\bigl(\exists i \in \mathbb{N}, \forall j \ge i,\ f_j \le x\bigr) \Rightarrow \operatorname{mk}(f) \le x$$$

Lean4

theorem mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) : mk f ≤ x :=
  by
  obtain ⟨i, H⟩ := h
  rw [← neg_le_neg_iff, ← mk_neg]
  exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩

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