closure — Mathlib

English

For any set s, membership in its closure, when viewed as a Closed, is equivalent to membership in the usual closure.

Русский

Для множества s принадлежность его замыканию, когда оно рассматривается как замкнутое, эквивалентна принадлежности обычному замыканию.

LaTeX

$$$ x \in Closeds.closure s \; \Leftrightarrow\; x \in closure s$$

Lean4

/-- The closure of a set, as an element of `TopologicalSpace.Closeds`. -/
@[simps]
protected def closure (s : Set α) : Closeds α :=
  ⟨closure s, isClosed_closure⟩

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