Carleson/ToMathlib/Analysis/RCLike/Misc.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem RCLike.enorm_eq_enorm_embedRCLike line 13 source

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

    Statement uses: RCLike, NNReal, Eq, ENNReal, ENorm.enorm, Function.comp, Real, RingHom, Algebra.algebraMap

    Proof uses: Eq.mpr, ENNReal.ofReal, Norm.norm, id, congrArg, Eq.symm, ofReal_norm, of_eq_true, Eq.trans, True, congr, norm_algebraMap', NNReal.abs_eq, ENNReal.ofReal_coe_nnreal, enorm_NNReal, eq_self

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. theorem RCLike.aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike line 19 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, RCLike, NNReal, Iff, MeasureTheory.AEStronglyMeasurable, Function.comp, Real, RingHom, Algebra.algebraMap

    Proof uses: Iff.intro, Eq, funext, of_eq_true, eq_self, Eq.mp, congrArg, propext, Topology.IsEmbedding.aestronglyMeasurable_comp_iff, Isometry.isEmbedding, congrFun, ENNReal, EDist.edist, rfl, algebraMap_isometry, Continuous.comp_aestronglyMeasurable, RCLike.continuous_ofReal, NNReal.continuous_coe

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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