Theorems · Theorem · general topology

DeltaGeneratedSpace.continuous_iff

Deprecated since 2026-04-23Use Topology.IsGeneratedBy.continuous_iff instead.

∀ {ι : 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 g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)

Alias of Topology.IsGeneratedBy.continuous_iff.

Defined in

Mathlib.Topology.Compactness.DeltaGeneratedSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopology.IsGeneratedBy