FLT/Mathlib/MeasureTheory/Measure/Regular.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Regular

Material destined for Mathlib.

Imports (2)
Imported by 1 file
  1. lemma Topology.IsOpenEmbedding.outerRegular_comap line 30 source

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

    Statement uses: TopologicalSpace, MeasurableSpace, BorelSpace, Topology.IsOpenEmbedding, MeasureTheory.Measure, MeasureTheory.Measure.OuterRegular, MeasureTheory.Measure.comap

    Proof uses: MeasureTheory.Measure.OuterRegular.mk, Set, MeasurableSet, ENNReal, GT.gt, And, GE.ge, Set.image, IsOpen, LT.lt, Exists, MeasureTheory.Measure.OuterRegular.outerRegular, MeasurableEmbedding.measurableSet_image', Topology.IsOpenEmbedding.measurableEmbedding, Eq.mp, congrArg, MeasurableEmbedding.comap_apply, Exists.intro, Set.preimage, And.intro and 11 more

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  2. lemma Topology.IsOpenEmbedding.innerRegularWRT_comap line 42 source

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

    Statement uses: TopologicalSpace, MeasurableSpace, BorelSpace, Topology.IsOpenEmbedding, MeasureTheory.Measure, MeasureTheory.Measure.InnerRegularWRT, IsCompact, IsOpen, MeasureTheory.Measure.comap

    Proof uses: Set, ENNReal, LT.lt, And, LE.le, Set.image, Exists, Iff.mp, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Eq.mp, congrArg, MeasurableEmbedding.comap_apply, Topology.IsOpenEmbedding.measurableEmbedding, Set.range, subset_trans, Set.image_subset_range, Exists.intro, Set.preimage, And.intro, Eq.mpr and 11 more

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  3. lemma Topology.IsOpenEmbedding.regular_comap line 56 source

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

    Statement uses: TopologicalSpace, MeasurableSpace, BorelSpace, Topology.IsOpenEmbedding, MeasureTheory.Measure, MeasureTheory.Measure.Regular, MeasureTheory.Measure.comap

    Proof uses: MeasureTheory.Measure.Regular.mk, Topology.IsOpenEmbedding.isFiniteMeasureOnCompacts_comap, Topology.IsOpenEmbedding.outerRegular_comap, Topology.IsOpenEmbedding.innerRegularWRT_comap, MeasureTheory.Measure.Regular.innerRegular

    2 instances, coercions and auxiliary constants left out.