Theorems · Theorem · general topology
Topology.IsGeneratedBy.iSup
∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {κ : Sort u_2}
{t : κ → TopologicalSpace Y}, (∀ (k : κ), Topology.IsGeneratedBy X Y) → Topology.IsGeneratedBy X YSuprema of X-generated topologies are X-generated.
- Defined in
- Mathlib.Topology.Convenient.GeneratedBy
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- LE.le.transproof · cited by 3,151
- iSupstatement · cited by 2,415
- le_iSupproof · cited by 207
- iSup_le_iffproof · cited by 45
- Topology.IsGeneratedBystatement and proof · cited by 38
- Topology.IsGeneratedBy.le_generatedByproof · cited by 3
- TopologicalSpace.generatedBy_monoproof · cited by 2
- Topology.IsGeneratedBy.iff_le_generatedByproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Topology.IsGeneratedBy.supproof · cited by 1
- DeltaGeneratedSpace.iSupproof · cited by 0