inv_eq_of_pos

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.inv_eq_of_pos

English

If x > 0, then x^{-1} = inv' x.

Русский

Если x > 0, то x^{-1} = inv' x.

LaTeX

$$$ 0 < x \Rightarrow x^{-1} = inv'\ x $$$

Lean4

theorem inv_eq_of_pos {x : PGame} (h : 0 < x) : x⁻¹ = inv' x := by
  classical exact (if_neg h.lf.not_equiv').trans (if_pos h)

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

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

Разделы

Аффилиация

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