lt_iff_exists_coe_btwn — Mathlib

English

Assume Preorder α, densely ordered α, NoMinOrder α. For a,b ∈ WithBot α, a < b iff there exists x ∈ α with a < ↑x and ↑x < b.

Русский

Пусть α упорядочено предикатно, плотно и без минимального элемента. Для a,b ∈ WithBot α выполняется a < b тогда и только тогда, когда существует x ∈ α такое, что a < ↑x и ↑x < b.

LaTeX

$$$a < b \iff \exists x : \alpha, a < ↑x \land ↑x < b$$$

Lean4

theorem lt_iff_exists_coe_btwn [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} :
    a < b ↔ ∃ x : α, a < ↑x ∧ ↑x < b :=
  ⟨fun h =>
    let ⟨_, hy⟩ := exists_between h
    let ⟨x, hx⟩ := lt_iff_exists_coe.1 hy.1
    ⟨x, hx.1 ▸ hy⟩,
    fun ⟨_, hx⟩ => lt_trans hx.1 hx.2⟩

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