closure_subtype — Mathlib

English

The closure of a subset in a subtype corresponds to the closure of its image in the ambient space.

Русский

Замыкание множества в подтипе соответствует замыканию образа множества в исходном пространстве.

LaTeX

$$$\text{closure}_{\text{Subtype}}(s) \leftrightarrow \text{closure}(\operatorname{image}(\text{Subtype.val}, s)).$$$

Lean4

theorem closure_subtype {x : { a // p a }} {s : Set { a // p a }} :
    x ∈ closure s ↔ (x : X) ∈ closure (((↑) : _ → X) '' s) :=
  closure_induced

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