inv_inv — Mathlib

English

If an element a of EReal is neither bottom nor top, then taking inverses twice returns the original element: (a^{−1})^{−1} = a.

Русский

Если элемент a в EReal не равен нижнему ни верхнему, то дважды взятие обратного возвращает исходный элемент: (a^{−1})^{−1} = a.

LaTeX

$$$ \forall a \in \mathrm{EReal},\ a \neq \bot \wedge a \neq \top \Rightarrow (a^{-1})^{-1} = a $$$

Lean4

theorem inv_inv {a : EReal} (h : a ≠ ⊥) (h' : a ≠ ⊤) : (a⁻¹)⁻¹ = a := by
  rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]

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