domain_mkSpanSingleton

Mathlib.LinearAlgebra.LinearPMap

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

English

The domain of the map mkSpanSingleton' x y H is R ∙ x.

Русский

Область определения mkSpanSingleton' x y H равна R∙x.

LaTeX

$$$\\mathrm{domain}(\\mathrm{mkSpanSingleton}'(x,y,H))=R\\cdot x$$$

Lean4

@[simp]
theorem domain_mkSpanSingleton (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) :
    (mkSpanSingleton' x y H).domain = R ∙ x :=
  rfl

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

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

Разделы

Аффилиация

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