Theorems · Inductive type · general topology

Topology.IsGeneratedBy

{ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → (Y : Type v) → [tY : TopologicalSpace Y] → Prop

Given a family of topological spaces X i, we say that a topological space is X-generated (IsGeneratedBy X Y) when the topology on Y is the X-generated topology, i.e. when the identity is a homeomorphism WithGeneratedByTopology X Y ≃ₜ Y (see IsGeneratedBy.homeomorph).

Defined in

Mathlib.Topology.Convenient.GeneratedBy

Cited by

38 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace