predAbove_left_inj

Mathlib.Order.Fin.Basic

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

← MathLib Explorer

English

For x, y ∈ Fin n, x.predAbove = y.predAbove iff x = y.

Русский

Для x, y ∈ Fin(n) выполняется x.predAbove = y.predAbove тогда и только тогда, когда x = y.

LaTeX

$$$\forall {x y : \mathrm{Fin}(n)}, x.predAbove = y.predAbove \iff x = y$$$

Lean4

/-- `predAbove` is injective at the pivot -/
@[simp]
theorem predAbove_left_inj {x y : Fin n} : x.predAbove = y.predAbove ↔ x = y :=
  predAbove_left_injective.eq_iff

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

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

Разделы

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

Аффилиация

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