sSup — Mathlib

English

sSup(c) denotes the least upper bound of a directed set c of LinearPMap under pointwise order.

Русский

sSup(c) обозначает наименьшее верхнее границу направленного множества LinearPMap по точному порядку.

LaTeX

$$$$ \\mathrm{sSup}(c) \\text{ представляет собой наименьшее верхнее границу по порядку }(\\mathrm{LinearPMap}, \\le). $$$$

Lean4

protected noncomputable def sSup (c : Set (E →ₗ.[R] F)) (hc : DirectedOn (· ≤ ·) c) : E →ₗ.[R] F :=
  ⟨_, Classical.choose <| sSup_aux c hc⟩

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