support_single_ne_bot — Mathlib

English

Let i ∈ α and b ≠ 0 in M. Then the support of the finitely supported function that is b at i and 0 elsewhere is nonempty.

Русский

Пусть i ∈ α и b ≠ 0 в M. Тогда опора функции, принимающей значение b в i и равной нулю в остальных точках, непуста.

LaTeX

$$$\operatorname{supp}(\mathrm{single}(i,b)) \neq \emptyset$$$

Lean4

theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥ := by
  simpa only [support_single_ne_zero _ h] using singleton_ne_empty _

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