Theorems · Theorem · general topology

OrderTopology.continuous_iff

∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α]
  [inst_2 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ ∀ (a : α), IsOpen (f ⁻¹' Set.Ioi a) ∧ IsOpen (f ⁻¹' Set.Iio a)

Defined in

Mathlib.Topology.Order.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderOrderTopologyTopologicalSpace