Theorems · Theorem · general topology

IsOpen.isGeneratedBy

∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_3}
  [inst_1 : TopologicalSpace Y] [∀ (i : ι) (U : TopologicalSpace.Opens (X i)), Topology.IsGeneratedBy X ↥U]
  [Topology.IsGeneratedBy X Y] {U : Set Y}, IsOpen U → Topology.IsGeneratedBy X ↑U

Defined in

Mathlib.Topology.Convenient.OpenClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopology.IsGeneratedByTopology.IsGeneratedBy