instDiscreteTopologySubtype — Mathlib

English

If X has a topology and is discrete, then the subtype {x | p x} has discrete topology.

Русский

Если X имеет топологию и дискретна, то подтип {x | p x} дискретен.

LaTeX

$$$ \\operatorname{DiscreteTopology}(\\operatorname{Subtype}(p)). $$$

Lean4

instance {p : X → Prop} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (Subtype p) :=
  ⟨bot_unique fun s _ => ⟨(↑) '' s, isOpen_discrete _, preimage_image_eq _ Subtype.val_injective⟩⟩

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