fromFunctionField_restrict — Mathlib

English

Restricting to a dense open preserves the function field description of a partial map: (f|_U).fromFunctionField = f.fromFunctionField.

Русский

Ограничение до плотной открытой подмножества сохраняет определение функционального поля частичной карты: (f|_U).fromFunctionField = f.fromFunctionField.

LaTeX

$$$$ (f.restrict U hU hU').fromFunctionField = f.fromFunctionField $$$$

Lean4

theorem fromFunctionField_restrict (f : X.PartialMap Y) [IrreducibleSpace X] {U : X.Opens} (hU : Dense (U : Set X))
    (hU' : U ≤ f.domain) : (f.restrict U hU hU').fromFunctionField = f.fromFunctionField :=
  fromSpecStalkOfMem_restrict f _ _ _

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