Theorems · Theorem · general topology
TopologicalSpace.Opens.mem_iSup
∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} {x : α} {s : ι → TopologicalSpace.Opens α},
x ∈ iSup s ↔ ∃ i, x ∈ s i- Defined in
- Mathlib.Topology.Sets.Opens
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 72 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.
Cites5
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
- iSupstatement · cited by 2,415
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- SetLike.mem_coeproof · cited by 302
- TopologicalSpace.Opens.coe_iSupproof · cited by 24
Cited by17
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.of_affine_open_coverproof · cited by 3
- AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpenproof · cited by 2
- PrimeSpectrum.toPiLocalization_surjective_of_discreteTopologyproof · cited by 2
- AlgebraicGeometry.Scheme.exists_isQuasiAffine_of_isLimitproof · cited by 1
- TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimageproof · cited by 1
- AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIsoproof · cited by 1
- AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIsoproof · cited by 1
- TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopologyproof · cited by 1
- AlgebraicGeometry.Proj.iSup_basicOpen_eq_topproof · cited by 1
- TopCat.Presheaf.toTypes_isSheafproof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.le_of_iSup_eq_topproof · cited by 1
- AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iffproof · cited by 1