Theorems · Theorem · general topology

Topology.IsOpenEmbedding.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] {F : Type u_4} [inst_4 : TopologicalSpace F] {f : F → Y},
  Topology.IsOpenEmbedding f → Topology.IsGeneratedBy X F

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: TopologicalSpace TopologicalSpace Topology.IsGeneratedBy Topology.IsGeneratedBy TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Set.Elemproof · cited by 7,166
Set.rangeproof · cited by 4,705
TopologicalSpace.Opensstatement and proof · cited by 2,040
Homeomorph.symmproof · cited by 365
Topology.IsOpenEmbeddingstatement and proof · cited by 231
Topology.IsOpenEmbedding.toIsEmbeddingproof · cited by 61
Topology.IsGeneratedBystatement and proof · cited by 38
Topology.IsOpenEmbedding.isOpen_rangeproof · cited by 33
Homeomorph.isQuotientMapproof · cited by 22
Topology.IsEmbedding.toHomeomorphproof · cited by 16
Topology.IsQuotientMap.isGeneratedByproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.