Theorems · Definition · algebraic geometry

AlgebraicGeometry.opensRestrict

{X : AlgebraicGeometry.Scheme} → (U : X.Opens) → (↑U).Opens ≃ { V // V ≤ U }

The open sets of an open subscheme corresponds to the open sets containing in the subset.

Defined in

Mathlib.AlgebraicGeometry.Restrict

Cited by

2 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound