exists_forall_le — Mathlib

English

Re-statement: (iSup f).N = sup_i (f i).N.

Русский

Переформулировка: (iSup f).N = sup_i (f i).N.

LaTeX

$$(iSup f).N = ⨆ i, (f i).N$$

Lean4

theorem exists_forall_le (h : F.Stable) (e : F.N 0 ≤ F'.N 0) : ∃ n₀, ∀ n, F.N (n + n₀) ≤ F'.N n :=
  by
  obtain ⟨n₀, hF⟩ := h
  use n₀
  intro n
  induction n with
  | zero => refine (F.antitone ?_).trans e; simp
  | succ n hn =>
    rw [add_right_comm, ← hF]
    · exact (smul_mono_right _ hn).trans (F'.smul_le _)
    simp

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