English
If each β i has no maximal element, then the lexicographic order on the dependent product ∀ i, β i has no maximal element.
Русский
Если у каждого β i нет максимального элемента, то в лексикографическом порядке на зависимом произведении ∀ i, β i тоже нет максимального элемента.
LaTeX
$$$[\text{Preorder } \iota] \land [\forall i, LT(\beta i)] \Rightarrow \left(\forall i, NoMaxOrder(\beta i)\right) \Rightarrow NoMaxOrder(\mathrm{Lex}(\forall i,\beta i))$$$
Lean4
theorem noMaxOrder' [Preorder ι] [∀ i, LT (β i)] (i : ι) [NoMaxOrder (β i)] : NoMaxOrder (Lex (∀ i, β i)) :=
⟨fun a => by
let ⟨b, hb⟩ := exists_gt (a i)
classical
exact
⟨Function.update a i b, i, fun j hj => (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩⟩
