inv

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#SetRel.InfiniteDimensional.inv

English

If r is InfiniteDimensional, then r.inv is InfiniteDimensional.

Русский

Если r бесконечно размерно, то r.inv тоже бесконечно размерно.

LaTeX

$$$$ \\operatorname{InfiniteDimensional}(r) \\Rightarrow \\operatorname{InfiniteDimensional}(r^{-1}). $$$$

Lean4

instance inv [InfiniteDimensional r] : InfiniteDimensional r.inv :=
  ⟨fun n ↦ ⟨.reverse (.withLength r n), RelSeries.length_withLength r n⟩⟩

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

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

Разделы

Аффилиация

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