range_succAbove

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

The range of p.succAbove is all of Fin(n+1) except p.

Русский

Образ p.succAbove совпадает со всем Fin(n+1), кроме p.

LaTeX

$$$\forall n \in \mathbb{N},\ Set.range(p.succAbove) = \{p\}^c.$$$

Lean4

/-- The range of `p.succAbove` is everything except `p`. -/
@[simp]
theorem range_succAbove (p : Fin (n + 1)) : Set.range p.succAbove = { p }ᶜ :=
  Set.ext fun _ => exists_succAbove_eq_iff

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

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

Разделы

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

Аффилиация

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