English
If ι is nonempty and each π(i) is Preorder with NoMaxOrder, then the space of all functions ∀ i, π(i) has NoMaxOrder.
Русский
Если индексное множество ι непусто и каждый π(i) — частично упорядованное множество без максимума, то множество функций ∀ i, π(i) тоже не имеет максимума.
LaTeX
$$$\forall ι, π:\, \big(\text{Nonempty}(ι) \land (\forall i, \text{Preorder}(π(i))) \land (\forall i, \text{NoMaxOrder}(π(i))) \Rightarrow \text{NoMaxOrder}(\, \forall i, π(i)\, )\big)$$$
Lean4
instance {ι : Type u} {π : ι → Type*} [Nonempty ι] [∀ i, Preorder (π i)] [∀ i, NoMaxOrder (π i)] :
NoMaxOrder (∀ i, π i) :=
⟨fun a => by
classical
obtain ⟨b, hb⟩ := exists_gt (a <| Classical.arbitrary _)
exact ⟨_, lt_update_self_iff.2 hb⟩⟩
