inv_mk — Mathlib

English

Inversion on a nonnegative element corresponds to inversion of the underlying value.

Русский

Инверсия над элементом неотрицательного множества соответствует инверсии его основанного значения.

LaTeX

$$$\\text{inv} \\langle x, 0 \\le x \\rangle = \\langle x^{-1}, \\text{inv\\_nonneg} \\; 0 \\le x \\rangle$$$

Lean4

@[simp]
theorem inv_mk (hx : 0 ≤ x) : (⟨x, hx⟩ : { x : α // 0 ≤ x })⁻¹ = ⟨x⁻¹, inv_nonneg.2 hx⟩ :=
  rfl

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