exists_partialMap_over — Mathlib

English

There exists a partial map g: X.PartialMap Y over S such that g.toRationalMap = f.

Русский

Существует частичная карта g: X.PartialMap Y над S такая, что g.toRationalMap = f.

LaTeX

$$$\forall X,Y,S\ f:X⟶Y \Rightarrow \exists g:X.PartialMap Y, g.IsOver S \wedge g.toRationalMap = f$$$

Lean4

theorem exists_partialMap_over [X.Over S] [Y.Over S] (f : X ⤏ Y) [f.IsOver S] :
    ∃ g : X.PartialMap Y, g.IsOver S ∧ g.toRationalMap = f :=
  IsOver.exists_partialMap_over

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