Theorems · Theorem · general topology
TopologicalSpace.Opens.coe_iSup
∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α),
↑(⨆ i, s i) = ⋃ i, ↑(s i)- Defined in
- Mathlib.Topology.Sets.Opens
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 71 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.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- SetLike.coestatement and proof · cited by 8,199
- Set.iUnionstatement and proof · cited by 2,483
- iSupstatement · cited by 2,415
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- Set.iUnion_congr_Propproof · cited by 374
- Set.iUnion_existsproof · cited by 45
- Set.iUnion_iUnion_eq'proof · cited by 21
Cited by24
Results whose statement or proof uses this declaration.
- TopologicalSpace.Opens.mem_iSupproof · cited by 17
- AlgebraicGeometry.iSup_affineOpens_eq_topproof · cited by 13
- TopologicalSpace.IsOpenCover.iSup_set_eq_univproof · cited by 11
- AlgebraicGeometry.Scheme.OpenCover.iSup_opensRangeproof · cited by 9
- PrimeSpectrum.iSup_basicOpen_eq_top_iffproof · cited by 6
- AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_topproof · cited by 5
- TopologicalSpace.Opens.iSup_defproof · cited by 5
- AlgebraicGeometry.Scheme.Hom.preimage_iSupproof · cited by 4
- MeasureTheory.Content.innerContent_iSup_natproof · cited by 3
- AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iffproof · cited by 2
- IsCompactOpenCovered.of_iUnion_eq_of_finiteproof · cited by 2
- AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_topproof · cited by 2