ContinuousPreimage

📁 Source: Mathlib/MeasureTheory/Measure/ContinuousPreimage.lean

Statistics

Metric	Count
Definitions	0
Theorems isClosed_setOf_preimage_ae_eq, tendsto_measure_symmDiff_preimage_nhds_zero	2
Total	2

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_setOf_preimage_ae_eq 📖	mathematical	Continuous ContinuousMap ContinuousMap.compactOpen MeasurePreserving DFunLike.coe ContinuousMap.instFunLike NullMeasurableSet	IsClosed setOf Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set.preimage	—	Measure.instOuterMeasureClass isOpen_compl_iff isOpen_iff_mem_nhds gt_mem_nhds ENNReal.instOrderTopology pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd measure_symmDiff_eq_zero_iff Filter.mp_mem Filter.Tendsto.eventually tendsto_measure_symmDiff_preimage_nhds_zero Continuous.tendsto Filter.Eventually.of_forall Filter.univ_mem' LT.lt.false symmDiff_comm measure_congr Filter.EventuallyEq.symmDiff ae_eq_refl
tendsto_measure_symmDiff_preimage_nhds_zero 📖	mathematical	Filter.Tendsto ContinuousMap nhds ContinuousMap.compactOpen Filter.Eventually MeasurePreserving DFunLike.coe ContinuousMap.instFunLike NullMeasurableSet	ENNReal Measure Set Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Set.preimage ENNReal.instTopologicalSpace instZeroENNReal	—	MeasurePreserving.map_eq Measure.InnerRegularCompactLTTop.map_of_continuous ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass ENNReal.tendsto_nhds_zero MeasurePreserving.measure_preimage Nat.instAtLeastTwoHAddOfNat MeasurableSet.exists_isCompact_isClosed_diff_lt MeasurePreserving.measurable IsOpen.measurableSet BorelSpace.opensMeasurable LT.lt.ne' IsClosed.nullMeasurableSet Filter.mp_mem ContinuousMap.tendsto_nhds_compactOpen Filter.univ_mem' ENNReal.add_halves LE.le.trans measure_symmDiff_le symmDiff_of_ge Set.MapsTo.subset_preimage symmDiff_of_le add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add ne_top_of_le_ne_top measure_mono Measure.instOuterMeasureClass measure_diff_le_iff_le_add LT.lt.le le_of_lt ENNReal.div_pos ENNReal.coe_ne_top NullMeasurableSet.exists_isOpen_symmDiff_lt MeasurableSet.nullMeasurableSet LT.lt.ne add_le_add_left Set.preimage_symmDiff NullMeasurableSet.symmDiff symmDiff_comm ENNReal.add_thirds

---

← Back to Index