NYLL
Module

Finite_compl_of_isOpen.lean

Nyll.AlgebraicCurves.Models.Finite_compl_of_isOpen
1 declaration indexed from sourceView source ↗

Module documentation

Finite compl of isOpen

The complement of an open subset of a curve is finite when the open contains the generic point.

Imports2
Imported by9

Declarations

theorem

finite_compl_of_isOpen

L30 ↗
AlgebraicCurve.finite_compl_of_isOpen
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Finite_compl_of_isOpen
universe u
open CategoryTheory AlgebraicGeometry Topology TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicCurve.finite_compl_of_isOpen
    {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [SmoothOfRelativeDimension 1 c] [QuasiCompact c]
    (U : C.Opens) (hU : (U : Set C).Nonempty) :
    ((U : Set C)ᶜ).Finite

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.