English
Let (α, ≤) be a partially ordered set with no maximal element. Then the upper set { x ∈ α : a ≤ x } (for any a ∈ α) has no maximal element as well, i.e., for every x with a ≤ x there exists y with a ≤ y and x < y.
Русский
Пусть (α, ≤) - частично упорядченное множество без максимального элемента. Тогда верхнее множество { x ∈ α : a ≤ x } для любого a ∈ α тоже не имеет максимального элемента: для каждого x с a ≤ x найдется y с a ≤ y и x < y.
LaTeX
$$$\\forall x \\in \\alpha,\\ a \\le x \\Rightarrow \\exists y \\in \\alpha\\ (a \\le y \\land x < y)$$$
Lean4
instance noMaxOrder [PartialOrder α] [NoMaxOrder α] {a : α} : NoMaxOrder { x : α // a ≤ x } :=
show NoMaxOrder (Ici a) by infer_instance
