orderClosedTopology' — Mathlib

English

Function space α → β inherits OrderClosedTopology from β when α has a preorder and β has OrderClosedTopology.

Русский

Пространство функций α → β наследует OrderClosedTopology от β при наличии преднаследования в α и OrderClosedTopology β.

LaTeX

$$$\text{OrderClosedTopology}(\alpha \to \beta).$$$

Lean4

instance orderClosedTopology' [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] : OrderClosedTopology (α → β) :=
  inferInstance

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