Theorems · Theorem · algebraic geometry

AlgebraicGeometry.sigmaOpenCover_f

∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] (b : σ),
  (AlgebraicGeometry.sigmaOpenCover g).f b = CategoryTheory.Limits.Sigma.ι g b

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

1 results in Mathlib

Foundations

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

Assumes

Small