Theorems · Theorem · functional analysis

MeasureTheory.GridLines.T.congr_simp

∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)]
  (μ μ_1 : (i : ι) → MeasureTheory.Measure (A i)),
  μ = μ_1 →
    ∀ {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] (p p_1 : ℝ),
      p = p_1 →
        ∀ (f f_1 : ((i : ι) → A i) → ENNReal),
          f = f_1 →
            ∀ (s s_1 : Finset ι),
              s = s_1 →
                ∀ (a a_1 : (i : ι) → A i),
                  a = a_1 → MeasureTheory.GridLines.T μ p f s a = MeasureTheory.GridLines.T μ_1 p_1 f_1 s_1 a_1

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEq