lt_iff_exists_coe_btwn — Mathlib

English

For Preorder α, densely ordered α, NoMaxOrder α, and a,b ∈ WithTop α, a < b iff there exists x in α with a < ↑x and ↑x < b.

Русский

Для предупорядоченного α, плотно упорядоченного α и NoMaxOrder α, и для a,b ∈ WithTop α, a < b тогда и только тогда, когда существует x∈α такое, что a < ↑x и ↑x < b.

LaTeX

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

Lean4

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

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