Mathlib Map

Theorems · Theorem · functional analysis

lp.ext

∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : ↥(lp E p)},
  ↑f = ↑g → f = g
Defined in
Mathlib.Analysis.Normed.Lp.lpSpace
Cited by
11 results in Mathlib
Foundations
Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

lp.ext_iff · cited by 1lp.ext_ifflp.single_neg · cited by 1lp.single_neglp.single_smul · cited by 1lp.single_smullp.toAddMonoidHom_linearMapOfLE · cited by 0lp.toAddMonoidHom_linearM…lp.zeroBasis_apply · cited by 0lp.zeroBasis_applylp.single_add · cited by 0lp.single_addlp.norm_eq_zero_iff · cited by 0lp.norm_eq_zero_iffLipschitzOnWith.extend_lp_infty · cited by 0LipschitzOnWith.extend_lp…lp.single_sub · cited by 0lp.single_sublp.single_zero · cited by 0lp.single_zerolp.linearMapOfLE_comp · cited by 0lp.linearMapOfLE_compNormedAddCommGroup · cited by 15752NormedAddCommGroupENNReal · cited by 9879ENNRealAddSubgroup · cited by 3232AddSubgroupPreLp · cited by 163PreLplp · cited by 157lplp.extCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • NormedAddCommGroupstatement and proof · cited by 15,752
  • ENNRealstatement and proof · cited by 9,879
  • AddSubgroupstatement · cited by 3,232
  • PreLpstatement and proof · cited by 163
  • lpstatement and proof · cited by 157

Cited by11

Results whose statement or proof uses this declaration.