toCloseds — Mathlib

English

Reinterpret a clopen as a closed: toCloseds maps a clopen to the closed set with the same carrier.

Русский

Переопределение clopen как замкнутого множества: toCloseds переводит clopen в замкнутое множество с тем же носителем.

LaTeX

$$$ \\text{toCloseds}(s) = \\langle s, s.isClosed \\rangle. $$$

Lean4

/-- Reinterpret a clopen as a closed. -/
@[simps]
def toCloseds (s : Clopens α) : Closeds α :=
  ⟨s, s.isClosed⟩

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