support_nonempty — Mathlib

English

If ι is nonempty and 2 ≠ 0 in R, then the support of the base b is nonempty.

Русский

Если индексный набор ι непуст и 2 ≠ 0 в R, то опорa базиса b непустая.

LaTeX

$$$[Nonempty\\ ι][NeZero\\ (2:R)]\\Rightarrow b.support.Nonempty$$$

Lean4

theorem support_nonempty [Nonempty ι] [NeZero (2 : R)] : b.support.Nonempty :=
  by
  by_contra! contra
  rw [Finset.not_nonempty_iff_eq_empty] at contra
  inhabit ι
  simpa [P.ne_zero default, contra] using b.root_mem_or_neg_mem default

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