isBoundedUnder_iff_eventually_bddAbove

English

For f on β and u: β → α with α a preordered set, f is bounded above by u iff there exists a set s with BddAbove(u[s]) and ∀ᶠ x in f, x ∈ s.

Русский

Для f на β и u: β → α с упорядоченным множеством α, f ограничен сверху относительно u тогда и только тогда, когда существует множество s такое, что BddAbove(u[s]) и ∀ᶠ x в f, x ∈ s.

LaTeX

$$$ f.IsBoundedUnder (\le) u \iff \exists s, BddAbove (u'' s) \land \forall^\infty x \in f, x \in s $$$

Lean4

theorem isBoundedUnder_iff_eventually_bddAbove :
    f.IsBoundedUnder (· ≤ ·) u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ x in f, x ∈ s :=
  by
  constructor
  · rintro ⟨b, hb⟩
    exact ⟨{a | u a ≤ b}, ⟨b, by rintro _ ⟨a, ha, rfl⟩; exact ha⟩, hb⟩
  · rintro ⟨s, ⟨b, hb⟩, hs⟩
    exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩

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