upperBounds_closure — Mathlib

English

In a space with ClosedIicTopology, the upper bounds of the closure of s coincide with those of s: upperBounds(closure s) = upperBounds(s).

Русский

В пространстве с ClosedIicTopology верхние границы closure(s) совпадают с верхними границами s: upperBounds(closure s) = upperBounds(s).

LaTeX

$$upperBounds(closure(s)) = upperBounds(s)$$

Lean4

@[simp]
theorem upperBounds_closure (s : Set α) : upperBounds (closure s : Set α) = upperBounds s :=
  ext fun a ↦ by simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

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