lt_one_iff

Mathlib.Algebra.Group.Fin.Basic

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

English

For x in Fin(n+2), x < 1 iff x = 0.

Русский

Для x из Fin(n+2) выполняется x < 1 тогда и только тогда, когда x = 0.

LaTeX

$$$\\forall n\\, (x\\in \\mathrm{Fin}(n+2)):\\; x<1 \\iff x=0$$$

Lean4

@[simp]
theorem lt_one_iff {n : ℕ} (x : Fin (n + 2)) : x < 1 ↔ x = 0 := by simp [lt_iff_val_lt_val]

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

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

Разделы

Аффилиация

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