instTopologicalSpaceFin

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#instTopologicalSpaceFin

English

For every n, Fin(n) is endowed with the indiscrete topology (only ∅ and Fin(n) are open).

Русский

Для любого n пространство Fin(n) имеет индиcкретную топологию (открыты только ∅ и всё пространство).

LaTeX

$$$\mathcal{O}(\mathrm{Fin}(n)) = \{ \varnothing, \mathrm{Fin}(n) \}$$$

Lean4

instance {n} : TopologicalSpace (Fin n) :=
  ⊥

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

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

Разделы

Аффилиация

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