le_rev_iff

Mathlib.Data.Fin.Rev

URI: https://scilib.ai/kg/mathlib#Fin.le_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 \le \mathrm{rev}(j) \iff j \le \mathrm{rev}(i).$$$

Lean4

theorem le_rev_iff {i j : Fin n} : i ≤ rev j ↔ j ≤ rev i := by rw [← rev_le_rev, rev_rev]

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

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

Разделы

Аффилиация

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