Theorems · Theorem · general topology

TopologicalSpace.IsTopologicalBasis.continuous_iff

∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] {B : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {f : α → β}, Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)

Defined in

Mathlib.Topology.Bases

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace