exists_le' — Mathlib

English

If s is dense and hbot: every bot element is in s, then for every x there exists y ∈ s with y ≤ x.

Русский

Если s плотно и выполняется условие, что любой минимальный элемент принадлежит s, то для каждого x существует y ∈ s с y ≤ x.

LaTeX

$$$\text{Dense}(s) \rightarrow (\forall x, \text{IsBot}(x) \rightarrow x \in s) \rightarrow \forall x, \exists y \in s, y \le x$$$

Lean4

theorem exists_le' {s : Set α} (hs : Dense s) (hbot : ∀ x, IsBot x → x ∈ s) (x : α) : ∃ y ∈ s, y ≤ x :=
  hs.orderDual.exists_ge' hbot x

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