minimal_mem_Ico — Mathlib

English

Let α be a partially ordered set and a < b. Then x is the minimal element of the half-open interval Ico(a,b) iff x = a.

Русский

Пусть α—частично упорядоченное множество и a < b. Тогда x — минимальный элемент полуоткрытого интервала Ico(a,b) тогда и только тогда, когда x = a.

LaTeX

$$$ a < b \\implies \\big( x \\in \\mathrm{Ico}(a,b) \\land \\forall y \\in \\mathrm{Ico}(a,b), y \\le x \\Rightarrow y = x \\big) \\iff x = a $$$

Lean4

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

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