Theorems · Theorem · general topology

Topology.IsGeneratedBy.coinduced

∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [Topology.IsGeneratedBy X Y] (f : Y → Z), Topology.IsGeneratedBy X Z

Any topology coinduced by an X-generated topology is X-generated.

Defined in: Mathlib.Topology.Convenient.GeneratedBy
Cited by: 2 results in Mathlib
Foundations: Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace Topology.IsGeneratedBy

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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
TopologicalSpace.coinducedstatement and proof · cited by 56
Topology.IsGeneratedBystatement and proof · cited by 38
continuous_coinduced_rngproof · cited by 19
Continuous.coinduced_leproof · cited by 4
Topology.IsGeneratedBy.equiv_symm_comp_continuous_iffproof · cited by 4
Topology.IsGeneratedBy.iff_le_generatedByproof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

Topology.IsQuotientMap.isGeneratedByproof · cited by 3
DeltaGeneratedSpace.coinducedproof · cited by 0