sSupFun — Mathlib

English

For a directed set c of partials, any f in c satisfies f.val ≤ sSupFun hc; that is, the supremum under directedness dominates each member.

Русский

Для направленного множества частичных отображений c всякое f ∈ c удовлетворяет неравенству f.val ≤ sSupFun hc.

LaTeX

$$$f.\\mathrm{val} \\le sSupFun\\; hc$ (при $f\\in c$)$$

Lean4

/-- A partial linear map that contains every element in a directed set of
`HahnEmbedding.Partial`. -/
noncomputable def sSupFun {c : Set (Partial seed)} (hc : DirectedOn (· ≤ ·) c) :
    M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R) :=
  LinearPMap.sSup ((·.val) '' c) (hc.mono_comp (by simp))

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