isBoundedUnder_iff_eventually_bddBelow

English

Analogous to above, but with ≥ replaced by ≤, i.e., f is bounded under ≥ by u iff ∃ s with BddBelow(u''s) and ∀ᶠ x in f, x ∈ s.

Русский

Аналогично, но с нижней границей: f ограничен снизу относительно u тогда и только тогда, когда существует s, для которого BddBelow(u''s) и ∀ᶠ x в f, x ∈ s.

LaTeX

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

Lean4

theorem isBoundedUnder_iff_eventually_bddBelow :
    f.IsBoundedUnder (· ≥ ·) u ↔ ∃ s, BddBelow (u '' s) ∧ ∀ᶠ x in f, x ∈ s :=
  isBoundedUnder_iff_eventually_bddAbove (α := αᵒᵈ)

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