instTopologicalSpaceSubtype — Mathlib

English

The topology on a Subtype p induced by the ambient space X via the inclusion map is well-defined.

Русский

Топология на подмножество {x ∈ X | p(x)} индуцируется включением из X и корректна.

LaTeX

$$TopologicalSpace (Subtype p) = induced (↑) t, where t is the topology on X$$

Lean4

instance _root_.instTopologicalSpaceSubtype {p : X → Prop} [t : TopologicalSpace X] : TopologicalSpace (Subtype p) :=
  induced (↑) t

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