notBelow_isOpen — Mathlib

English

The notBelow set is open; i.e., its indicator is ωScottContinuous.

Русский

Множество notBelow открыто; индикаторная функция ωScott непрерывна.

LaTeX

$$$notBelow\_isOpen(y) : IsOpen(\text{notBelow}(y)).$$$

Lean4

@[deprecated isClosed_Iic (since := "2025-07-02")]
theorem notBelow_isOpen (y : Scott α) : IsOpen (notBelow y) :=
  by
  have h : Monotone (notBelow y) := fun x z hle ↦ mt hle.trans
  dsimp only [IsOpen, TopologicalSpace.IsOpen, Scott.IsOpen]
  rw [ωScottContinuous_iff_monotone_map_ωSup]
  refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩
  simp only [ωSup_le_iff, notBelow, mem_setOf_eq, le_Prop_eq, OrderHom.coe_mk, Chain.map_coe, Function.comp_apply,
    exists_imp, not_forall]

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