unbounded_ge_univ — Mathlib

English

Let α be a partial order with no bottom element. Then for every a there exists b such that a ≥ b.

Русский

Пусть α обладает частичным порядком и не имеет нижней границы. Тогда для каждого a существует b, такой что a ≥ b.

LaTeX

$$$\forall a,\exists b:\ a \ge b$$$

Lean4

theorem unbounded_ge_univ [LE α] [NoBotOrder α] : Unbounded (· ≥ ·) (@Set.univ α) := fun a =>
  let ⟨b, hb⟩ := exists_not_ge a
  ⟨b, ⟨⟩, hb⟩

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