isOpen_iff_scottContinuous_mem — Mathlib

English

Let α be a preorder. If α is endowed with a topology and isScott on univ, then a set s is open iff the indicator function x ↦ x ∈ s is Scott-continuous.

Русский

Пусть α — предварительное упорядочение. Если на α задана топология и α являетсяScott при рассмотрении всей области, то множество s открыто тогда и только тогда, когда индикаторная функция x ↦ (x ∈ s) скоттовски непрерывна.

LaTeX

$$$\text{IsOpen}(s) \iff \text{ScottContinuous}(\lambda x. x \in s).$$$

Lean4

theorem isOpen_iff_scottContinuous_mem [Preorder α] {s : Set α} [TopologicalSpace α] [IsScott α univ] :
    IsOpen s ↔ ScottContinuous fun x ↦ x ∈ s :=
  by
  rw [← scottContinuousOn_univ, scottContinuousOn_iff_continuous (fun _ _ _ ↦ by trivial)]
  exact isOpen_iff_continuous_mem

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