Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Metric.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 2 files
  1. lemma MeasureTheory.NoAtoms'.of_metric line 23 source

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

    Statement uses: PseudoMetricSpace, ProperSpace, MeasurableSpace, OpensMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasureOnCompacts, Real, Eq, ENNReal, Set, Metric.closedBall, Metric.ball, MeasureTheory.NoAtoms'

    Proof uses: Eq.mpr, MeasurableSet, LT.lt, OfNat.ofNat, Exists, And, LE.le, id, congrArg, propext, MeasureTheory.no_atoms_iff, Inter.inter, Monotone, MeasureTheory.measure_mono, Set.inter_subset_inter_left, Metric.ball_subset_ball, Membership.mem, Set.Ici, iSup, Set.Iio and 118 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 94 steps

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

  2. instance MeasureTheory.NoAtoms'.(instance at line 107) line 107 source
  3. instance MeasureTheory.NoAtoms'.(instance at line 117) line 117 source