toOpens — Mathlib

English

Reinterpret a clopen as an open: toOpens maps a clopen to the open set with the same carrier.

Русский

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

LaTeX

$$$ \\text{toOpens}(s) = \\langle s, s.isOpen \\rangle. $$$

Lean4

/-- Reinterpret a clopen as an open. -/
@[simps]
def toOpens (s : Clopens α) : Opens α :=
  ⟨s, s.isOpen⟩

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