rev_eq_iff

Mathlib.Data.Fin.Rev

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

English

Equality under reversal is symmetric: rev i = j iff i = rev j.

Русский

Равенство после разворота симметрично: rev i = j ⇔ i = rev j.

LaTeX

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

Lean4

theorem rev_eq_iff {i j : Fin n} : rev i = j ↔ i = rev j := by rw [← rev_inj, rev_rev]

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

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

Разделы

Аффилиация

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