inv_Ioo_0_left — Mathlib

English

For a > 0, the inverse image under inversion of Ioo(0, a) is Ioi(a^{-1}).

Русский

Для a > 0 образ под действием инверсии множества Ioo(0, a) равен Ioi(a^{-1}).

LaTeX

$$$ (Ioo(0,a))^{-1} = Ioi(a^{-1}) $$$

Lean4

/-- The (pre)image under `inv` of `Ioo 0 a` is `Ioi a⁻¹`. -/
theorem inv_Ioo_0_left (ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹ :=
  by
  ext x
  exact
    ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2, fun h ↦
      ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩

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