univ_nontrivial — Mathlib

English

Let α be a finite nontrivial type. Then the universal finite set in α contains at least two distinct elements; equivalently there exist a,b ∈ α with a ≠ b.

Русский

Пусть α — конечный непустой тип с двумя различными элементами; тогда Finset.univ α содержит по крайней мере два различных элемента, то есть существуют a,b ∈ α, такие что a ≠ b.

LaTeX

$$$\exists x \in \mathrm{univ}, \exists y \in \mathrm{univ}, x \neq y$$$

Lean4

theorem univ_nontrivial [h : Nontrivial α] : (Finset.univ : Finset α).Nontrivial :=
  univ_nontrivial_iff.mpr h

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