of_span₀ — Mathlib

English

If span R s and span R t are disjoint and 0 ∉ s, then s and t are disjoint.

Русский

Если span R s и span R t не пересекаются и 0 ∉ s, то s и t также не пересекаются.

LaTeX

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

Lean4

theorem _root_.Disjoint.of_span₀ (hst : Disjoint (span R s) (span R t)) (h0s : 0 ∉ s) : Disjoint s t :=
  by
  rw [← diff_singleton_eq_self h0s]
  exact hst.of_span

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