eq_top_iff_eq_one

Mathlib.Data.ENNReal.Holder

URI: https://scilib.ai/kg/mathlib#ENNReal.HolderConjugate.eq_top_iff_eq_one

Lean4

theorem eq_top_iff_eq_one : p = ∞ ↔ q = 1 := by
  constructor
  · rintro rfl
    rw [← inv_inv q, ← one_sub_inv ∞ q]
    simp
  · rintro rfl
    rw [← inv_inv p, ← one_sub_inv 1 p]
    simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru