subsingleton_zero_smul_set — Mathlib

English

With the same hypotheses as above, the image (0) • s is a subsingleton; in particular, (0 : α) • s has at most one element.

Русский

При тех же предположениях изображение (0) • s является подмножество с одним элементом; то есть вектор (0) • s имеет не более одного элемента.

LaTeX

$$$ ((0 : \alpha) \cdot s).\text{Subsingleton} $$$

Lean4

theorem subsingleton_zero_smul_set (s : Set β) : ((0 : α) • s).Subsingleton :=
  subsingleton_singleton.anti <| zero_smul_set_subset s

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