instOrderClosedTopologyProd — Mathlib

English

The space of all functions α → αi (a family) inherits order-closed topology from each coordinate, i.e., product topology preserves order-closed property.

Русский

Пространство всех функций образует произведение, сохраняющее свойство OrderClosedTopology по всем координатам.

LaTeX

$$$[\forall i, Preorder(α_i)]\ [\forall i, TopologicalSpace(α_i)]\ [\forall i, OrderClosedTopology(α_i)]\Rightarrow OrderClosedTopology\left(\prod_i α_i\right).$$$

Lean4

instance [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β]
    [OrderClosedTopology β] : OrderClosedTopology (α × β) :=
  ⟨(isClosed_le continuous_fst.fst continuous_snd.fst).inter (isClosed_le continuous_fst.snd continuous_snd.snd)⟩

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