rev_le_iff

Mathlib.Data.Fin.Rev

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

Lean4

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

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

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

Разделы

Аффилиация

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