unbounded_le_of_forall_exists_lt — Mathlib

English

In a preorder, if every element a is exceeded by some b in s (a < b), then s is unbounded for ≤.

Русский

В предпорядке, если для каждого a существует b в s с a < b, то s неограничено по ≤.

LaTeX

$$$[Preorder] (\forall a, \exists b\in s, a

Lean4

theorem unbounded_le_of_forall_exists_lt [Preorder α] (h : ∀ a, ∃ b ∈ s, a < b) : Unbounded (· ≤ ·) s := fun a =>
  let ⟨b, hb, hb'⟩ := h a
  ⟨b, hb, fun hba => hba.not_gt hb'⟩

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