isOpen_fold

Mathlib.Topology.Basic

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

English

The notion of open sets is the same whether written as IsOpen s or as IsOpen t s.

Русский

Понятие открытого множества не зависит от записи: IsOpen s или IsOpen t s дают одно и то же.

LaTeX

$$$t.IsOpen s = IsOpen[t] s$$$

Lean4

theorem isOpen_fold {t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s :=
  rfl

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

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

Разделы

Аффилиация

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