isOrtho_span — Mathlib

English

span(s) ⟂ span(t) iff all inner products ⟪u,v⟫ are zero for u ∈ s, v ∈ t.

Русский

span(s) ⟂ span(t) тогда и только тогда, когда для всех u ∈ s, v ∈ t выполнено ⟪u,v⟫ = 0.

LaTeX

$$\operatorname{span}(s) \perp \operatorname{span}(t) \iff \forall u \in s, \forall v \in t, \langle u,v \rangle = 0$$

Lean4

@[simp]
theorem isOrtho_span {s t : Set E} : span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u⦄, u ∈ s → ∀ ⦃v⦄, v ∈ t → ⟪u, v⟫ = 0 := by
  simp_rw [span_eq_iSup_of_singleton_spans s, span_eq_iSup_of_singleton_spans t, isOrtho_iSup_left, isOrtho_iSup_right,
    isOrtho_iff_le, span_le, Set.subset_def, SetLike.mem_coe, mem_orthogonal_singleton_iff_inner_left,
    Set.mem_singleton_iff, forall_eq]

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