Theorems · Theorem · general topology

Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff

∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] [Topology.IsGeneratedBy X Y] (g : Y → Z),
  Continuous (⇑Topology.WithGeneratedByTopology.equiv.symm ∘ g) ↔ Continuous g

Defined in

Mathlib.Topology.Convenient.GeneratedBy

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopology.IsGeneratedBy