maximal_mem_Icc — Mathlib

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)

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