two_two

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderConjugate.two_two

← MathLib Explorer

English

The pair (2,2) is Holder conjugate: 1/2 + 1/2 = 1.

Русский

Пара (2,2) образует конъюгат Холдера: 1/2 + 1/2 = 1.

LaTeX

$$$\tfrac{1}{2} + \tfrac{1}{2} = 1$$$

Lean4

theorem two_two : HolderConjugate 2 2
    where
  inv_add_inv_eq_inv := by simpa using add_halves (1 : ℝ≥0)
  left_pos := zero_lt_two
  right_pos := zero_lt_two

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

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

Разделы

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

Аффилиация

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