ProbabilityTheory.FiniteMeasure.sub_def🔗

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.sub_def.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} (μ ν : MeasureTheory.FiniteMeasure α) :
  μ - ν = ⟨↑μ - ↑ν, ⋯⟩
ProbabilityTheory.FiniteMeasure.sub_def.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  (μ ν : MeasureTheory.FiniteMeasure α) :
  μ - ν = ⟨↑μ - ↑ν, ⋯⟩

lemma FiniteMeasure.sub_def (μ ν : FiniteMeasure α) :
    μ - ν = ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩

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⟩⟩