length_withLength

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.length_withLength

← MathLib Explorer

English

For [r.InfiniteDimensional], the length of RelSeries.withLength r n is n.

Русский

При [r.InfiniteDimensional] длина RelSeries.withLength r n равна n.

LaTeX

$$$(RelSeries.withLength r n).length = n$$$

Lean4

@[simp]
theorem length_withLength [r.InfiniteDimensional] (n : ℕ) : (RelSeries.withLength r n).length = n :=
  (SetRel.InfiniteDimensional.exists_relSeries_with_length n).choose_spec

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

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

Разделы

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

Аффилиация

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