instDenselyOrderedLex — Mathlib

English

If α and β are densely ordered, then the lexicographic product Lex(α × β) is densely ordered as well.

Русский

Если α и β упорядочены плотно, то и лексикографическое произведение Lex(α × β) также плотно упорядочено.

LaTeX

$$$\\mathrm{DenselyOrdered}(\\mathrm{Lex}(\\alpha \\times \\beta)).$$$

Lean4

instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α ×ₗ β) where
  dense := by
    rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩)
    · obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(a, c), right _ h₁, right _ h₂⟩

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