instNontrivial

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.instNontrivial

English

If n ≥ 2, then Fin(n) is nontrivial (there exists more than one element).

Русский

Если n ≥ 2, то Fin(n) не тривиален (есть более чем одно элемент).

LaTeX

$$$$\text{If } n \ge 2,\; \mathrm{Nontrivial}(\mathrm{Fin}(n)).$$$$

Lean4

instance instNontrivial [n.AtLeastTwo] : Nontrivial (Fin n) :=
  nontrivial_iff_two_le.2 Nat.AtLeastTwo.one_lt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru