baseEmbedding_le_extendFun — Mathlib

English

There is a consistent extension of f by hx: the base embedding is below the extended function image: seed.baseEmbedding ≤ f.extendFun hx.

Русский

Существует консистентное продолжение f на hx: базовое вложение ниже образа расширенной функции.

LaTeX

$$$\\text{seed.baseEmbedding} \\le f.extendFun\\; hx$$$

Lean4

theorem baseEmbedding_le_extendFun [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) :
    seed.baseEmbedding ≤ f.extendFun hx := by
  rw [extendFun]
  exact le_trans f.prop.baseEmbedding_le <| LinearPMap.left_le_sup _ _ _

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