instNontrivial — Mathlib

English

If α is nonempty and M is nontrivial, then the finsupp space α →₀ M is nontrivial.

Русский

Если α непусто и M не тривиально, то пространство финсапп-функций α →₀ M не тривиально.

LaTeX

$$$\text{Nonempty}(\alpha) \land \text{Nontrivial}(M) \Rightarrow \text{Nontrivial}(\alpha \to_{0} M)$$$

Lean4

instance instNontrivial [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M) :=
  by
  inhabit α
  rcases exists_ne (0 : M) with ⟨x, hx⟩
  exact nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)

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