minimal_mem_Icc — Mathlib

English

In a partially ordered set, for a ≤ b, the minimal element of the closed interval [a,b] is a.

Русский

В частично упорядоченном множестве, если a ≤ b, минимальный элемент интервала [a,b] равен a.

LaTeX

$$$\\forall a,b,\\; a \\le b \\Rightarrow (\\operatorname{Minimal}(\\cdot \\in [a,b]) x) \\Leftrightarrow x = a$$$

Lean4

theorem minimal_mem_Icc (hab : a ≤ b) : Minimal (· ∈ Icc a b) x ↔ x = a :=
  minimal_iff_eq ⟨rfl.le, hab⟩ (fun _ ↦ And.left)

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