disjoint_span_singleton_of_notMem

Mathlib.LinearAlgebra.Span.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.disjoint_span_singleton_of_notMem

English

If x ≠ 0, then (Disjoint s (span{x})) is equivalent to x ∉ s.

Русский

Если x ≠ 0, то Disjoint s (span{x}) эквивалентно x ∉ s.

LaTeX

$$$Disjoint\, s\, (\operatorname{span}\;\{x\})' \iff x \notin s$$$

Lean4

theorem disjoint_span_singleton_of_notMem (hx : x ∉ s) : Disjoint s (K ∙ x) :=
  by
  rw [disjoint_span_singleton]
  intro h
  contradiction

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru