domain_supSpanSingleton

Mathlib.LinearAlgebra.LinearPMap

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

← MathLib Explorer

English

If every f ∈ c is ≤ g, then sSup c ≤ g.

Русский

Если каждая f из c ≤ g, то sSup c ≤ g.

LaTeX

$$$$ \\text{If } \\forall f \\in c, f \\le g, \\ \\mathrm{sSup}(c) \\le g. $$$$

Lean4

@[simp]
theorem domain_supSpanSingleton (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) :
    (f.supSpanSingleton x y hx).domain = f.domain ⊔ K ∙ x :=
  rfl

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

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

Разделы

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

Аффилиация

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