IndisputableMonolith.Compat.Mathlib

   1import Mathlib
   2
   3/-!
   4Compatibility shims and common mathlib imports.
   5
   6This module collects small alias lemmas and helpers to stabilize names
   7across mathlib versions and reduce duplication across the codebase.
   8-/
   9
  10open scoped BigOperators Matrix
  11open Real Complex
  12
  13-- Aliases and small helpers (avoid redefining Mathlib lemmas)
  14
  15theorem one_div_pos_of_pos' {x : ℝ} (hx : 0 < x) : 0 < 1 / x := by
  16  simpa [one_div] using inv_pos.mpr hx
  17
  18theorem one_div_nonneg_of_nonneg' {x : ℝ} (hx : 0 ≤ x) : 0 ≤ 1 / x := by
  19  simpa [one_div] using inv_nonneg.mpr hx
  20
  21theorem Real.rpow_nonneg_of_nonneg' {x a : ℝ} (hx : 0 ≤ x) : 0 ≤ x ^ a := by
  22  simpa using Real.rpow_nonneg hx a
  23
  24theorem Real.rpow_lt_one_of_pos_of_lt_one' {x y : ℝ}
  25    (hx_pos : 0 < x) (hx_lt_one : x < 1) (hy_pos : 0 < y) :
  26    x ^ y < 1 := by
  27  exact Real.rpow_lt_one hx_pos.le hx_lt_one hy_pos
  28
  29-- Common simp-normalizations for division forms
  30theorem one_div_mul' (x y : ℝ) : (1 / x) * y = y / x := by
  31  ring
  32
  33theorem inv_pos_iff_one_div_pos' {x : ℝ} : (0 < x⁻¹) ↔ (0 < 1 / x) := by
  34  simp [one_div]
  35