finiteDimensional_inv

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#SetRel.finiteDimensional_inv

English

FiniteDimensional r.inv iff FiniteDimensional r.

Русский

Конченная размерность r.inv эквивалентна конченой размерности r.

LaTeX

$$$$ \\operatorname{FiniteDimensional\_inv} : \\operatorname{FiniteDimensional}(r.inv) \\iff \\operatorname{FiniteDimensional}(r). $$$$

Lean4

@[simp]
theorem finiteDimensional_inv : FiniteDimensional r.inv ↔ FiniteDimensional r :=
  ⟨fun _ ↦ .inv r.inv, fun _ ↦ .inv _⟩

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

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

Разделы

Аффилиация

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