lt_rev_iff

Mathlib.Data.Fin.Rev

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

English

For i,j in Fin(n), i < rev j iff j < rev i.

Русский

Для i,j ∈ Fin(n) выполняется i < rev j ⇔ j < rev i.

LaTeX

$$$\forall i,j:\mathrm{Fin}(n),\ i<\mathrm{rev}(j)\iff j<\mathrm{rev}(i).$$$

Lean4

theorem lt_rev_iff {i j : Fin n} : i < rev j ↔ j < rev i := by rw [← rev_lt_rev, rev_rev]

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

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

Разделы

Аффилиация

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