ProbabilityTheory.FiniteMeasure.toMeasure_sub🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

ProbabilityTheory.FiniteMeasure.toMeasure_sub.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} (μ ν : MeasureTheory.FiniteMeasure α) :
  ↑(μ - ν) = ↑μ - ↑ν
ProbabilityTheory.FiniteMeasure.toMeasure_sub.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  (μ ν : MeasureTheory.FiniteMeasure α) :
  ↑(μ - ν) = ↑μ - ↑ν

lemma FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) = (↑μ - ↑ν : Measure α)

rfl

Dependency graph

Type dependencies (1)

ProbabilityTheory.instSubFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α} :
  Sub (MeasureTheory.FiniteMeasure α)
ProbabilityTheory.instSubFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1}
  {mα : MeasurableSpace α} :
  Sub (MeasureTheory.FiniteMeasure α)

noncomputable
instance : Sub (FiniteMeasure α)

⟨fun μ ν ↦ ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩⟩