image_succAbove_univ

Mathlib.Data.Fintype.Basic

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

English

For i : Fin (n+1), the image of univ under succAbove equals the complement of {i}.

Русский

Для i : Fin(n+1), образ univ под succAbove равен комплементу множества {i}.

LaTeX

$$$\mathrm{univ.image} \, i.\mathrm{succAbove} = {i}^{c}$$$

Lean4

@[simp]
theorem image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) : univ.image i.succAbove = { i }ᶜ :=
  by
  ext m
  simp

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

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

Разделы

Аффилиация

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