subsingleton_Icc_of_ge — Mathlib

English

Let α be a partially ordered set and a, b ∈ α with b ≤ a. Then the closed interval Icc(a, b) contains at most one element.

Русский

Пусть α — частично упорядченное множество, и a, b ∈ α такие, что b ≤ a. Тогда замкнутый интервал Icc(a, b) содержит не более одной точки.

LaTeX

$$$$ b \\le a \\implies \\forall x,y\\,\\big( x,y \\in Icc(a,b) \\Rightarrow x = y \\big). $$$$

Lean4

theorem subsingleton_Icc_of_ge (hba : b ≤ a) : Set.Subsingleton (Icc a b) := fun _x ⟨hax, hxb⟩ _y ⟨hay, hyb⟩ ↦
  le_antisymm (le_imp_le_of_le_of_le hxb hay hba) (le_imp_le_of_le_of_le hyb hax hba)

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