Theorems · Definition · general topology

TopologicalSpace.Opens.comap

{α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → C(α, β) → FrameHom (TopologicalSpace.Opens β) (TopologicalSpace.Opens α)

The preimage of an open set, as an open set.

Defined in

Mathlib.Topology.Sets.Opens

Cited by

32 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace