PFR/Mathlib/MeasureTheory/Measure/Dirac/Def.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma MeasureTheory.Measure.dirac_real_apply' line 11 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, Set, MeasurableSet, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.dirac, Set.indicator, OfNat.ofNat

    Proof uses: dite, Membership.mem, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, congrArg, ENNReal, MeasureTheory.Measure, ENNReal.toReal, MeasureTheory.Measure.dirac_apply', Set.indicator_of_mem, eq_self, Not, Set.indicator_of_notMem, False, eq_false, not_false_eq_true

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.