sSup — Mathlib

English

There exists a partial Hahn embedding whose domain equals the entire module.

Русский

Существует частичное Ган-встраивание, чья область определения совпадает со всем модулем.

LaTeX

$$$\\exists f : Partial seed, f.val.domain = \\top$$$

Lean4

/-- Promote `HahnEmbedding.Partial.sSupFun` to a `HahnEmbedding.Partial`. -/
noncomputable def sSup [IsOrderedAddMonoid R] {c : Set (Partial seed)} (hnonempty : c.Nonempty)
    (hc : DirectedOn (· ≤ ·) c) : Partial seed :=
  ⟨_, isPartial_sSupFun hnonempty hc⟩

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