subsingleton_Icc_iff — Mathlib

English

In a linear order, the closed interval Icc(a, b) is subsingleton if and only if b ≤ a.

Русский

В линейном порядке замкнутый интервал Icc(a, b) является одиночным тогда и только тогда, когда b ≤ a.

LaTeX

$$$$\\text{Icc}(a,b)\\text{ is subsingleton} \\;\\iff\\; b \\le a.$$$$

Lean4

@[simp]
theorem subsingleton_Icc_iff {α : Type*} [LinearOrder α] {a b : α} : Set.Subsingleton (Icc a b) ↔ b ≤ a :=
  by
  refine ⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩
  contrapose! h
  exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩

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