of_span — Mathlib

English

If span R s is disjoint from span R t, then s \ {0} is disjoint from t.

Русский

Если span R s и span R t не пересекаются, то s без нуля совместно с t не пересекаются.

LaTeX

$$$$\text{Disjoint}(\operatorname{span} R s, \operatorname{span} R t) \Rightarrow \text{Disjoint}(s \setminus \{0\}, t) $$$$

Lean4

theorem _root_.Disjoint.of_span (hst : Disjoint (span R s) (span R t)) : Disjoint (s \ {0}) t :=
  by
  rw [disjoint_iff_forall_ne]
  rintro v ⟨hvs, hv0 : v ≠ 0⟩ _ hvt rfl
  exact hv0 <| (disjoint_def.1 hst) v (subset_span hvs) (subset_span hvt)

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