Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.approxOn.congr_simp

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] (f f_1 : β → α) (e_f : f = f_1) (hf : Measurable f)
  (s s_1 : Set α) (e_s : s = s_1) (y₀ y₀_1 : α) (e_y₀ : y₀ = y₀_1) (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s] (n n_1 : ℕ),
  n = n_1 → MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n = MeasureTheory.SimpleFunc.approxOn f_1 ⋯ s_1 y₀_1 ⋯ n_1

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpaceMeasurableSpaceTopologicalSpace.SeparableSpace