instNoMinOrderForallOfNonempty — Mathlib

English

If ι is nonempty and each π(i) is Preorder with NoMinOrder, then the space of all functions ∀ i, π(i) has NoMinOrder.

Русский

Если ι непусто и каждый π(i) — упорядочено без минимума, то пространство функций ∀ i, π(i) также не имеет минимума.

LaTeX

$$$\forall ι, π:\, \big(\text{Nonempty}(ι) \land (\forall i, \text{Preorder}(π(i))) \land (\forall i, \text{NoMinOrder}(π(i))) \Rightarrow \text{NoMinOrder}(\, \forall i, π(i)\, )\big)$$$

Lean4

instance {ι : Type u} {π : ι → Type*} [Nonempty ι] [∀ i, Preorder (π i)] [∀ i, NoMinOrder (π i)] :
    NoMinOrder (∀ i, π i) :=
  ⟨fun a => by
    classical
    obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
    exact ⟨_, update_lt_self_iff.2 hb⟩⟩

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