le_sSup

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.le_sSup

← MathLib Explorer

English

If f ∈ c, then f ≤ sSup c.

Русский

Если f ∈ c, то f ≤ sSup c.

LaTeX

$$$$ f \\le \\mathrm{sSup}(c) \\quad \\text{ whenever } f \\in c. $$$$

Lean4

protected theorem le_sSup {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {f : E →ₗ.[R] F} (hf : f ∈ c) :
    f ≤ LinearPMap.sSup c hc :=
  Classical.choose_spec (sSup_aux c hc) hf

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru