Theorems · Definition · general topology

Homeomorph.opensCongr

{α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → α ≃ₜ β → TopologicalSpace.Opens α ≃o TopologicalSpace.Opens β

A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps.

Defined in

Mathlib.Topology.Sets.Opens

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace