isPartial_extendFun — Mathlib

English

Extend f by hx to obtain a larger partial embedding; the result is again a partial embedding with its own strict monotonicity and range properties.

Русский

Расширим частичное отображение f на hx: получится большее частичное вложение, сохраняющее строго монотонность и свойства диапазона.

LaTeX

$$$\\text{extendFun}\\; hx : (\\text{Partial seed})$ isPartial_extendFun$$

Lean4

theorem isPartial_extendFun [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) :
    IsPartial seed (extendFun f hx) where
  strictMono := f.extendFun_strictMono hx
  baseEmbedding_le := f.baseEmbedding_le_extendFun hx
  truncLT_mem_range := f.truncLT_mem_range_extendFun hx

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