instIsOverToPartialMapOfIsSeparatedOfIsOver

English

If a rational map f is over S, so is its associated partial map.

Русский

Если рациональная карта f над S, то и соответствующая ей частичная карта над S.

LaTeX

$$$$ \text{IsOver}_S(f) \Rightarrow \text{IsOver}_S\left( f^{\mathrm{toPartialMap}}\right). $$$$

Lean4

instance [IsReduced X] [Y.IsSeparated] [S.IsSeparated] [X.Over S] [Y.Over S] (f : X ⤏ Y) [f.IsOver S] :
    f.toPartialMap.IsOver S :=
  by
  rw [← PartialMap.isOver_toRationalMap_iff_of_isSeparated, f.toRationalMap_toPartialMap]
  infer_instance

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