lt_extend — Mathlib

English

If x is not in the domain, then f is strictly less than its extension: f < f.extend hx.

Русский

Если x не лежит в области определения, то f строго меньше своего расширения: f < f.extend hx.

LaTeX

$$$f < f.extend\\; hx$$$

Lean4

theorem lt_extend [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) : f < f.extend hx :=
  by
  apply lt_of_le_of_ne
  · change f.val ≤ (f.extend hx).val
    simpa [extend, extendFun] using LinearPMap.left_le_sup _ _ _
  by_contra!
  have : f.val.domain = (f.extend hx).val.domain := by congr
  rw [this] at hx
  contrapose! hx with h
  simpa using Submodule.mem_sup_right (by simp)

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