equivSubtype

Mathlib.Data.Fin.Basic

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

← MathLib Explorer

English

There is a natural bijection between Fin n and { i // i < n }.

Русский

Существует естественная биекция между Fin n и { i | i < n }.

LaTeX

$$$Fin(n) \cong \{ i \mid i < n \}$$$

Lean4

/-- Equivalence between `Fin n` and `{ i // i < n }`. -/
@[simps apply symm_apply]
def equivSubtype : Fin n ≃ { i // i < n } where
  toFun a := ⟨a.1, a.2⟩
  invFun a := ⟨a.1, a.2⟩

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

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

Разделы

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

Аффилиация

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