preimage_comp — Mathlib

English

For morphisms f: X→Y and g: Y→Z and x in X, the base map of the composition equals applying g after f to x: (f ≫ g).base x = g.base (f.base x).

Русский

Для морфизмов f: X→Y и g: Y→Z и элемента x ∈ X, отображение основания композиции равно применению g после f к x: (f ≫ g).base x = g.base (f.base x).

LaTeX

$$$(f \\gg g).base\\; x = g.base (f.base\\; x)$$$

Lean4

@[simp]
theorem preimage_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (f ≫ g) ⁻¹ᵁ U = f ⁻¹ᵁ g ⁻¹ᵁ U :=
  rfl

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