instIsUpperProd — Mathlib

English

The upper topology on a product is obtained by dualizing the lower-product construction.

Русский

Верхняя топология на произведении получаются путем дуализации конструирования нижней топологии на произведении.

LaTeX

$$$IsUpper(\alpha \times \beta)$$$

Lean4

instance instIsUpperProd [Preorder α] [TopologicalSpace α] [IsUpper α] [OrderTop α] [Preorder β] [TopologicalSpace β]
    [IsUpper β] [OrderTop β] : IsUpper (α × β) where
  topology_eq_upperTopology :=
    by
    suffices IsLower (α × β)ᵒᵈ from IsLower.topology_eq_lowerTopology (α := (α × β)ᵒᵈ)
    exact instIsLowerProd (α := αᵒᵈ) (β := βᵒᵈ)

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