AlgebraicGeometry.exists_isAffineOpen_le_inf_forall_mem_of_finset
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_le_inf_forall_mem_of_finset
universe u
open CategoryTheory AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.exists_isAffineOpen_le_inf_forall_mem_of_finset
{X : Scheme.{u}} (W : X.Opens) (hW : IsAffineOpen W) (O : X.Opens) (F : Finset X)
(hFW : ∀ x ∈ F, x ∈ W) (hFO : ∀ x ∈ F, x ∈ O) :
∃ W' : X.Opens, IsAffineOpen W' ∧ W' ≤ W ⊓ O ∧ ∀ x ∈ F, x ∈ W'