isClosed

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#Finset.isClosed

English

A finite subset of a topological space is closed.

Русский

Конечное подмножество топологического пространства замкнуто.

LaTeX

$$$\\forall X [\\mathcal{T}_1(X)] \\; \\forall s : Finite, IsClosed(s.toSet).$$$

Lean4

protected theorem isClosed [T1Space X] (s : Finset X) : IsClosed (s : Set X) :=
  s.finite_toSet.isClosed

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

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

Разделы

Аффилиация

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