Theorems · Theorem · algebraic geometry
AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le
∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
AlgebraicGeometry.IsAffineOpen U → ∀ {V : X.Opens} (x : ↥V), ↑x ∈ U → ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f- Defined in
- Mathlib.AlgebraicGeometry.AffineScheme
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites47
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Top.topproof · cited by 9,680
- CategoryTheory.Functor.mapproof · cited by 8,698
- SetLike.coeproof · cited by 8,199
- Oppositestatement · cited by 8,081
- CategoryTheory.Iso.homproof · cited by 7,684
- CategoryTheory.Iso.invproof · cited by 6,514
- Set.imageproof · cited by 5,609
- Set.rangeproof · cited by 4,705
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
Cited by5
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.exists_basicOpen_le_affine_interproof · cited by 7
- AlgebraicGeometry.Scheme.exists_le_and_germ_injectiveproof · cited by 3
- AlgebraicGeometry.isBasis_preimage_isAffineOpenproof · cited by 1
- AlgebraicGeometry.isAffineHom_of_isInducingproof · cited by 0
- AlgebraicGeometry.exists_affineOpens_le_appLE_of_appLEproof · cited by 0