gramSchmidt_zero

Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

URI: https://scilib.ai/kg/mathlib#InnerProductSpace.gramSchmidt_zero

English

If all input vectors are zero, GramSchmidt outputs zero vectors for every index.

Русский

Если входные векторы все нули, GramSchmidt возвращает нулевые векторы для каждого индекса.

LaTeX

$$$ \text{gramSchmidt}_{\mathbb{K}}(f)(n) = 0 \quad \text{for all } n$$$

Lean4

@[simp]
theorem gramSchmidt_zero (n : ι) : gramSchmidt 𝕜 (0 : ι → E) n = 0 := by rw [gramSchmidt_def]; simp

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

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

Разделы

Аффилиация

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