frontier_Icc — Mathlib

English

If a ≤ b in a densely ordered space with both min and max absent, the frontier of the closed interval Icc(a,b) is the set {a,b}.

Русский

При a ≤ b в плотно упорядоченном пространстве без минимума и максимума граница закрытого интервала Icc(a,b) равна {a,b}.

LaTeX

$$$\operatorname{frontier}(\mathrm{Icc}(a,b)) = \{a,b\}$$$

Lean4

@[simp]
theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) : frontier (Icc a b) = { a, b } := by
  simp [frontier, h, Icc_diff_Ioo_same]

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