le_orthogonalBilin_orthogonalBilin

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.le_orthogonalBilin_orthogonalBilin

English

As above (duplicate entry of reflexivity implication).

Русский

Как выше (повторное соотношение рефлексивности).

LaTeX

$$$\text{B.IsRefl} \Rightarrow N \le (N.orthogonalBilin B).orthogonalBilin B$$$

Lean4

theorem le_orthogonalBilin_orthogonalBilin (b : B.IsRefl) : N ≤ (N.orthogonalBilin B).orthogonalBilin B :=
  fun n hn _m hm ↦ b _ _ (hm n hn)

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

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

Разделы

Аффилиация

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