coe_conjExponent — Mathlib

English

For p > 1, p.conjExponent = conjExponent p.

Русский

Для p > 1 конъюгированная экспонента ENNReal совпадает с экспонентой NNReal.

LaTeX

$$p.conjExponent = conjExponent p$$

Lean4

theorem coe_conjExponent {p : ℝ≥0} (hp : 1 < p) : p.conjExponent = conjExponent p :=
  by
  rw [NNReal.conjExponent, conjExponent]
  norm_cast
  rw [← coe_inv (tsub_pos_of_lt hp).ne']
  norm_cast
  field_simp [(tsub_pos_of_lt hp).ne']
  rw [tsub_add_cancel_of_le hp.le]

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