affineSpan_eq_bot — Mathlib

English

The affine span is the bottom subspace if and only if the set is empty.

Русский

Аффинная оболочка равна нулевому подпроизведению тогда и только тогда, когда множество пусто.

LaTeX

$$$\operatorname{affineSpan}(k, s) = \bot \iff s = \emptyset$$$

Lean4

/-- The affine span of a set is `⊥` if and only if that set is empty. -/
@[simp]
theorem affineSpan_eq_bot : affineSpan k s = ⊥ ↔ s = ∅ := by
  rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty, nonempty_iff_ne_empty]

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