Theorems · Theorem · general topology

Topology.IsClosedEmbedding.isGeneratedBy

∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_3}
  [inst_1 : TopologicalSpace Y] [∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), Topology.IsGeneratedBy X ↥F]
  [Topology.IsGeneratedBy X Y] {U : Type u_4} [inst_4 : TopologicalSpace U] {f : U → Y},
  Topology.IsClosedEmbedding f → Topology.IsGeneratedBy X U

Defined in

Mathlib.Topology.Convenient.OpenClosed

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopology.IsGeneratedByTopology.IsGeneratedByTopologicalSpace