mem_orthogonalBilin_iff

Mathlib.LinearAlgebra.SesquilinearForm.Basic

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

English

If B is reflexive, then N is contained in its double orthogonal: N ≤ (N.orthogonalBilin B).orthogonalBilin B.

Русский

Если B рефлексивна, то N ⊆ (N⊥_B)⊥_B.

LaTeX

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

Lean4

@[simp]
theorem mem_orthogonalBilin_iff {m : M₁} : m ∈ N.orthogonalBilin B ↔ ∀ n ∈ N, B.IsOrtho n m :=
  Iff.rfl

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

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

Разделы

Аффилиация

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