instDenselyOrderedColexForall — Mathlib

English

If ι is a Preorder, and each β i is LT and densely ordered, then the colef-lex order on ∀ i, β i is densely ordered.

Русский

Если ι — предорядок, а для каждого i β i LT и плотно упорядован, то Colex (∀ i, β i) плотно упорядован.

LaTeX

$$$[\text{Preorder } \iota] \land [\forall i, LT(\beta i)] \land [\forall i, DenselyOrdered(\beta i)] \Rightarrow \ DenselyOrdered(\mathrm{Colex}(\forall i,\beta i))$$$

Lean4

instance [Preorder ι] [∀ i, LT (β i)] [∀ i, DenselyOrdered (β i)] : DenselyOrdered (Colex (∀ i, β i)) :=
  inferInstanceAs (DenselyOrdered (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))

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