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]