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]