erase_nonempty — Mathlib

English

If a finite set s is nontrivial (has at least two distinct elements), then removing any element a yields a nonempty set.

Русский

Если множество s не тривиально (есть хотя бы два разных элемента), то удаление любого элемента a оставляет непустое множество.

LaTeX

$$$$ s\text{ nontrivial } \Rightarrow (s\setminus\{a\}) \neq \emptyset. $$$$

Lean4

protected theorem erase_nonempty (hs : s.Nontrivial) : (s.erase a).Nonempty :=
  (hs.exists_ne a).imp <| by simp_all

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