Theorems · Theorem · general topology

induced_topology_eq_preorder

∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace β] [OrderTopology β]
  {f : α → β},
  (∀ {x y : α}, f x < f y ↔ x < y) →
    (∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y) →
      (∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b) →
        TopologicalSpace.induced f inst_2 = Preorder.topology α

Defined in

Mathlib.Topology.Order.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

PreorderPreorderTopologicalSpaceOrderTopology