finSuccEquiv'_eq_none

Mathlib.Logic.Equiv.Fin.Basic

URI: https://scilib.ai/kg/mathlib#finSuccEquiv'_eq_none

← MathLib Explorer

English

Equality to None is equivalent to i = j: finSuccEquiv' i j = none ⇔ i = j.

Русский

Равенство None эквивалентно i = j: finSuccEquiv' i j = none ⇔ i = j.

LaTeX

$$$\\text{finSuccEquiv'}\\ i\\ j = \\mathrm{none} \\iff i = j$$$

Lean4

@[simp]
theorem finSuccEquiv'_eq_none {i j : Fin (n + 1)} : finSuccEquiv' i j = none ↔ i = j :=
  (finSuccEquiv' i).apply_eq_iff_eq_symm_apply.trans eq_comm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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