English
The product of two lower-topology spaces carries a lower topology.
Русский
Произведение пространств с нижней топологией оснащено нижней топологией.
LaTeX
$$$IsLower(\alpha \times \beta)$$$
Lean4
instance instIsLowerProd [Preorder α] [TopologicalSpace α] [IsLower α] [OrderBot α] [Preorder β] [TopologicalSpace β]
[IsLower β] [OrderBot β] : IsLower (α × β) where
topology_eq_lowerTopology := by
refine le_antisymm (le_generateFrom ?_) ?_
· rintro _ ⟨x, rfl⟩
exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl
rw [(IsLower.isTopologicalBasis.prod IsLower.isTopologicalBasis).eq_generateFrom, le_generateFrom_iff_subset_isOpen,
image2_subset_iff]
rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
dsimp
simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]
-- without `let`, `refine` tries to use the product topology and fails
let _ : TopologicalSpace (α × β) := lower (α × β)
refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)
· exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
· exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩
