instOrderClosedTopologyForall — Mathlib

English

Instance asserting the product of two order-closed topological spaces has order-closed topology.

Русский

Инстанс: произведение двух пространств с OrderClosedTopology также имеет OrderClosedTopology.

LaTeX

$$$\operatorname{OrderClosedTopology}(\alpha \times \beta).$$$

Lean4

instance {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, OrderClosedTopology (α i)] : OrderClosedTopology (∀ i, α i) :=
  by
  constructor
  simp only [Pi.le_def, setOf_forall]
  exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

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