rev_lt_iff

Mathlib.Data.Fin.Rev

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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