NYLL
Module

Scheme_OrderedAffineCover_nonempty_of_compactSpace.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_OrderedAffineCover_nonempty_of_compactSpace
1 declaration indexed from sourceView source ↗

Module documentation

Scheme Ordered Affine Cover nonempty of compact Space

Imports2
Imported by4

Declarations

theorem

nonempty_of_compactSpace

L29 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.nonempty_of_compactSpace
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCover_nonempty_of_compactSpace
open AlgebraicGeometry CategoryTheory TopologicalSpace
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.OrderedAffineCover.nonempty_of_compactSpace (V :
  Scheme.{u}) [CompactSpace V] : Nonempty V.OrderedAffineCover

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