Theorems · Theorem · order theory

Topology.IsScott.scottContinuousOn_iff_continuous

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Preorder β]
  [inst_3 : TopologicalSpace β] [Topology.IsScott β Set.univ] {f : α → β} {D : Set (Set α)} [Topology.IsScott α D],
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) → (ScottContinuousOn D f ↔ Continuous f)

Defined in

Mathlib.Topology.Order.ScottTopology

Cited by

2 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderTopologicalSpacePreorderTopologicalSpaceTopology.IsScottTopology.IsScott