Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.norm_approxBounded_le

∀ {α : Type u_1} {β : Type u_5} {f : α → β} [inst : SeminormedAddCommGroup β] [inst_1 : NormedSpace ℝ β]
  {m : MeasurableSpace α} {c : ℝ} (hf : MeasureTheory.StronglyMeasurable f),
  0 ≤ c → ∀ (n : ℕ) (x : α), ‖(hf.approxBounded c n) x‖ ≤ c

Defined in: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: SeminormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites33

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

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
NormedSpacestatement and proof · cited by 12,499
Norm.normstatement and proof · cited by 5,413
LE.le.transproof · cited by 3,151
one_mulproof · cited by 2,841
SeminormedAddCommGroupstatement and proof · cited by 2,671
mul_commproof · cited by 2,262
MulZeroClass.mul_zeroproof · cited by 2,091
le_reflproof · cited by 2,061
mul_assocproof · cited by 1,667

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.condExp_stronglyMeasurable_bilin_of_boundproof · cited by 3