le_of_exists — Mathlib

English

If there exists i with f(j) ≤ g(j) for all j ≥ i, then f ≤ g.

Русский

Если существует i такое, что f(j) ≤ g(j) для всех j ≥ i, то f ≤ g.

LaTeX

$$$\bigl(\exists i, \forall j \ge i,\; f(j) \le g(j)\bigr) \Rightarrow f \le g.$$$

Lean4

theorem le_of_exists {f g : CauSeq α abs} (h : ∃ i, ∀ j ≥ i, f j ≤ g j) : f ≤ g :=
  let ⟨i, hi⟩ := h
  (or_assoc.2 (CauSeq.lt_total f g)).elim id fun hgf =>
    False.elim
      (let ⟨_, hK0, j, hKj⟩ := hgf
      not_lt_of_ge (hi (max i j) (le_max_left _ _)) (sub_pos.1 (lt_of_lt_of_le hK0 (hKj _ (le_max_right _ _)))))

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