English
In a partially ordered set, for a ≤ b, the maximal element of [a,b] is b.
Русский
В частично упорядоченном множестве, если a ≤ b, максимальный элемент интервала [a,b] равен b.
LaTeX
$$$\\forall a,b,\\; a \\le b \\Rightarrow (\\operatorname{Maximal}(\\cdot \\in [a,b]) x) \\Leftrightarrow x = b$$$
Lean4
theorem maximal_mem_Icc (hab : a ≤ b) : Maximal (· ∈ Icc a b) x ↔ x = b :=
maximal_iff_eq ⟨hab, rfl.le⟩ (fun _ ↦ And.right)