instFrame

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.instFrame

English

The collection of open sets forms a frame under inclusion.

Русский

Множество открытых подмножеств образует фрейм по включению.

LaTeX

$$$ \text{Opens}(\alpha) \text{ is a frame} $$$

Lean4

instance instFrame : Frame (Opens α) :=
  .ofMinimalAxioms frameMinimalAxioms

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

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

Разделы

Аффилиация

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