instDiscreteTopology

Mathlib.Topology.List

URI: https://scilib.ai/kg/mathlib#List.instDiscreteTopology

English

If α has a discrete topology, then List α has a discrete topology.

Русский

Если у α дискретная топология, то List α также дискретна.

LaTeX

$$$ [\text{DiscreteTopology}(\alpha)] \Rightarrow \operatorname{DiscreteTopology}(\operatorname{List}(\alpha)) $$$

Lean4

instance [DiscreteTopology α] : DiscreteTopology (List α) := by rw [discreteTopology_iff_nhds]; intro l;
  induction l <;> simp [*, nhds_cons]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru