instNontrivial — Mathlib

English

If α is nonempty, then Finset α is nontrivial; i.e., there exist two distinct Finsets of α.

Русский

Если множество α непустое, то Finset α не тривиально: существуют две различные конечные подмножества α.

LaTeX

$$$(\exists x,y \in \text{Finset }\alpha)\, x \neq y$ given $\alpha \neq \emptyset$$$

Lean4

instance instNontrivial [Nonempty α] : Nontrivial (Finset α) :=
  ‹Nonempty α›.elim fun a => ⟨⟨{ a }, ∅, singleton_ne_empty _⟩⟩

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