scottContinuous_iff_map_sSup — Mathlib

English

Scott continuity of a map f is equivalent to preservation of suprema of directed sets: f(sSup d) = sSup(f''d).

Русский

Скоттово непрерывность отображения f эквивалентна сохранению верхних граней по направленным множествам: f(sSup d) = sSup(f''d).

LaTeX

$$$\\text{ScottContinuous}(f) \\iff \\forall \\{d : \\mathrm{Set}(\\alpha)\\}, d.Nonempty \\to DirectedOn (\\le) d \\to f(\\mathrm{sup}\\, d) = \\mathrm{sup}(f'' d)$$$

Lean4

theorem scottContinuous_iff_map_sSup {f : α → β} :
    ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → f (sSup d) = sSup (f '' d)
    where
  mp h _ d₁ d₂ := by rw [IsLUB.sSup_eq (h d₁ d₂ (isLUB_iff_sSup_eq.mpr rfl))]
  mpr h _ d₁ d₂ _ hda := by rw [isLUB_iff_sSup_eq, ← (h d₁ d₂), IsLUB.sSup_eq hda]

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