rev_ne_iff

Mathlib.Data.Fin.Rev

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

English

Negation equivalence under reversal: rev i ≠ j iff i ≠ rev j.

Русский

Неравенство после разворота эквивалентно неравенству до разворота: rev i ≠ j ⇔ i ≠ rev j.

LaTeX

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

Lean4

theorem rev_ne_iff {i j : Fin n} : rev i ≠ j ↔ i ≠ rev j :=
  rev_eq_iff.not

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

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

Разделы

Аффилиация

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