symm

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderTriple.symm

← MathLib Explorer

English

If h is p.HolderTriple q r, then q.HolderTriple p r.

Русский

Если h : p.HolderTriple q r, то q.HolderTriple p r.

LaTeX

$$$\forall p,q,r \,(p.HolderTriple q r) \Rightarrow q.HolderTriple p r$$$

Lean4

@[symm]
protected theorem symm : q.HolderTriple p r
    where
  inv_add_inv_eq_inv := add_comm p⁻¹ q⁻¹ ▸ h.inv_add_inv_eq_inv
  left_pos := h.right_pos
  right_pos := h.left_pos

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

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

Разделы

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

Аффилиация

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