Carleson/ToMathlib/MeasureTheory/Function/AEEqFun.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem AEEqFun.mk_sum line 11 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, Finset, Membership.mem, MeasureTheory.AEStronglyMeasurable, Eq, MeasureTheory.AEEqFun, MeasureTheory.AEEqFun.mk, Finset.sum, Finset.aestronglyMeasurable_sum, Subtype, Finset.attach, Finset.coe_mem

    Proof uses: Finset.induction_on, Classical.propDecidable, EmptyCollection.emptyCollection, id, Eq.refl, OfNat.ofNat, Not, Insert.insert, Eq.mpr, HAdd.hAdd, AddCommMonoid, Finset.sum_insert, congrFun', congrArg, MeasureTheory.AEEqFun.mk.congr_simp, Finset.mem_insert_of_mem, Subtype.mk, Finset.mem_insert_self, Subtype.property, sum_attach_insert and 3 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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