inv_Ioo_0_right — Mathlib

English

For a < 0, the inverse of Iio a is Ioo a⁻¹ 0.

Русский

Для a < 0 обратный образ Iio a равен Ioo a⁻¹ 0.

LaTeX

$$$(\mathrm{Iio}(a))^{-1} = \mathrm{Ioo}(a^{-1},0)$$$

Lean4

/-- The (pre)image under `inv` of `Ioo a 0` is `Iio a⁻¹`. -/
theorem inv_Ioo_0_right {a : α} (ha : a < 0) : (Ioo a 0)⁻¹ = Iio a⁻¹ :=
  by
  ext x
  refine ⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩
  have h' := (h.trans (inv_neg''.2 ha))
  exact ⟨(lt_inv_of_neg ha h').2 h, inv_neg''.2 h'⟩

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