affineSpan_eq_top_iff_nonempty_of_subsingleton

English

If the ambient space is subsingleton, then the affine span equals the top iff the set is nonempty.

Русский

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

LaTeX

$$$\operatorname{affineSpan}(k, s) = \top \iff s \neq \emptyset$ (assuming Subsingleton).$$

Lean4

@[simp]
theorem affineSpan_eq_top_iff_nonempty_of_subsingleton [Subsingleton P] : affineSpan k s = ⊤ ↔ s.Nonempty := by
  rw [← bot_lt_affineSpan k, IsSimpleOrder.bot_lt_iff_eq_top]

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