instDenselyOrderedProd — Mathlib

English

If α and β are densely ordered, then their Cartesian product α × β with the product order is densely ordered.

Русский

Если два множества упорядочены плотно, то их декартово произведение упорядочено плотно по произведению порядка.

LaTeX

$$$DenselyOrdered(\alpha \times \beta)$$$

Lean4

instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α × β) :=
  ⟨fun a b ↦ by
    simp_rw [Prod.lt_iff]
    rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · obtain ⟨c, ha, hb⟩ := exists_between h₁
      exact ⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h₂
      exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩⟩

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