fst — Mathlib

English

If g is universally open, then the first projection from the fiber product X ×_Z Y → X is universally open.

Русский

Если g универсально открыто, то первая проекция из fibration X ×_Z Y → X является универсально открытой.

LaTeX

$$$\forall f:X\to Z,\; \forall g:Y\to Z, [\mathsf{UniversallyOpen}(g)]\Rightarrow \mathsf{UniversallyOpen}(\text{pullback.fst } f\, g).$$$

Lean4

instance fst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : UniversallyOpen g] : UniversallyOpen (pullback.fst f g) :=
  MorphismProperty.pullback_fst f g hg

Похожие утверждения