Theorems · Theorem · functional analysis

MeasureTheory.GridLines.T_empty

∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] {p : ℝ} (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i),
  MeasureTheory.GridLines.T μ p f ∅ x = f x ^ (1 + p)

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

1 results in Mathlib

Foundations

Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceDecidableEq