infiniteDimensional_inv

Mathlib.Order.RelSeries

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

English

InfiniteDimensional r.inv ↔ InfiniteDimensional r.

Русский

InfiniteDimensional r.inv ⇔ InfiniteDimensional r.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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