instTopologicalSpace — Mathlib

English

The topology on the set of points of the complete lattice L is defined by IsOpen s iff ∃ u, {x | x u} = s.

Русский

Топология на множестве точек полного решётки L задаётся так: открытое множество s тогда и только тогда, когда ∃ u, {x | x u} = s.

LaTeX

$$IsOpen(S) := ∃ u, {x | x u} = S$$

Lean4

/-- The topology on the set of points of the complete lattice `L`. -/
instance instTopologicalSpace : TopologicalSpace (PT L)
    where
  IsOpen s := ∃ u, {x | x u} = s
  isOpen_univ := ⟨⊤, by simp⟩
  isOpen_inter := by rintro s t ⟨u, rfl⟩ ⟨v, rfl⟩; use u ⊓ v; simp_rw [map_inf]; rfl
  isOpen_sUnion S
    hS := by
    choose f hf using hS
    use ⨆ t, ⨆ ht, f t ht
    simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]

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