directedAffineCover_trans — Mathlib

English

If U ≤ V for affine opens U, V in X, refining the directed affine cover along hUV yields the same result as the original refinement morphism.

Русский

Если U ≤ V для аффинных открытых участков U, V в X, уточнение направленного аффинного покрытия по hUV даёт тот же результат, что и исходное уточнение.

LaTeX

$$$$ \operatorname{Cover.Trans}(X.directedAffineCover, \mathrm{homOfLE}(hUV)) = X.homOfLE(hUV) $$$$

Lean4

@[simp]
theorem directedAffineCover_trans {U V : X.affineOpens} (hUV : U ≤ V) :
    Cover.trans X.directedAffineCover (homOfLE hUV) = X.homOfLE hUV :=
  rfl

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