English
Let α be a partially ordered set and a < b. Then x is the maximal element of the interval Ioc(a,b) iff x = b.
Русский
Пусть α — частично упорядоченное множество и a < b. Тогда x — максимальный элемент интервала Ioc(a,b) тогда и только тогда, когда x = b.
LaTeX
$$$ a < b \\implies \\big( x \\in \\mathrm{Ioc}(a,b) \\land \\forall y \\in \\mathrm{Ioc}(a,b), x \\le y \\Rightarrow y = x \\big) \\iff x = b $$$
Lean4
theorem maximal_mem_Ioc (hab : a < b) : Maximal (· ∈ Ioc a b) x ↔ x = b :=
maximal_iff_eq ⟨hab, rfl.le⟩
(fun _ ↦ And.right)
/- Note : The one-sided interval versions of these lemmas are unnecessary,
since `simp` handles them with `maximal_le_iff` and `minimal_ge_iff`. -/
