exists_eventually_atTop — Mathlib

English

There is an equivalence between the existence of a tail of r a b and a tail condition in atTop.

Русский

Существование условия в хвосте r a b эквивалентно хвостовому условию в atTop.

LaTeX

$$$ (\\exists b, \\forall^{\\mathrm{e}} a \\in \\mathrm{atTop}, r\,a\,b) \\iff \\forall^{\\mathrm{e}} a_0 \\in \\mathrm{atTop}, \\exists b, \\forall a \\ge a_0, r\,a\,b $$$

Lean4

theorem exists_eventually_atTop {r : α → β → Prop} :
    (∃ b, ∀ᶠ a in atTop, r a b) ↔ ∀ᶠ a₀ in atTop, ∃ b, ∀ a ≥ a₀, r a b :=
  by
  simp_rw [eventually_atTop, ← exists_swap (α := α)]
  exact exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦ H n (hb.trans hn)

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