mem_orthogonal' — Mathlib

English

v ∈ K⊥ iff ∀ u ∈ K, ⟪v, u⟫ = 0 by inner symmetry.

Русский

v ∈ K⊥ тогда и только тогда, когда для всех u ∈ K выполняется ⟪v, u⟫ = 0 (по симметрии скалярного произведения).

LaTeX

$$$$ v \in K^{\perp} \iff \forall u \in K, \langle v, u \rangle = 0. $$$$

Lean4

/-- When a vector is in `Kᗮ`, with the inner product the
other way round. -/
theorem mem_orthogonal' (v : E) : v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫ = 0 := by simp_rw [mem_orthogonal, inner_eq_zero_symm]

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