mem_orthogonal_iff — Mathlib

English

m ∈ B.orthogonal N if and only if m is orthogonal to every n ∈ N with respect to B.

Русский

m принадлежит B.orthogonal N тогда и только тогда, когда m ортогонален ко всем n ∈ N относительно B.

LaTeX

$$$ m \\in B.orthogonal N \\iff \\forall n \\in N, B.IsOrtho n m $$$

Lean4

@[simp]
theorem mem_orthogonal_iff {N : Submodule R M} {m : M} : m ∈ B.orthogonal N ↔ ∀ n ∈ N, IsOrtho B n m :=
  Iff.rfl

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