not_bddBelow_iff' — Mathlib

English

Not bounded below is equivalent to: for every x there exists y in s with x not ≤ y.

Русский

Не ограничено снизу эквивалентно: для каждого x существует y ∈ s such that x не ≤ y.

LaTeX

$$$\\lnot \\text{BddBelow}(s) \\iff \\forall x, \\exists y \\in s, \\lnot x \\le y$$$

Lean4

/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` such that `x`
is not less than or equal to `y`. This version only assumes `Preorder` structure and uses
`¬(x ≤ y)`. A version for linear orders is called `not_bddBelow_iff`. -/
theorem not_bddBelow_iff' : ¬BddBelow s ↔ ∀ x, ∃ y ∈ s, ¬x ≤ y :=
  @not_bddAbove_iff' αᵒᵈ _ _

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