Embedding

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

Statistics

Metric	Count
Definitions `MeasurableEmbedding`, `equivImage`, `equivRange`, `invFun`, `schroederBernstein`, `prod`, `rangeInl`, `rangeInr`, `singleton`, `univ`, `apply`, `symm_apply`, `arrowCongr'`, `arrowProdEquivProdArrow`, `cast`, `curry`, `finTwoArrow`, `funUnique`, `instEquivLike`, `instInhabited`, `ofInvolutive`, `ofUniqueOfUnique`, `piCongrLeft`, `piCongrRight`, `piCurry`, `piEquivPiSubtypeProd`, `piFinSuccAbove`, `piFinTwo`, `piFinsetUnion`, `piMeasurableEquivTProd`, `piOptionEquivProd`, `piUnique`, `prodAssoc`, `prodComm`, `prodCongr`, `prodPUnit`, `prodSumDistrib`, `punitProd`, `refl`, `setOf`, `sumCompl`, `sumCongr`, `sumPiEquivProdPi`, `sumProdDistrib`, `sumProdSum`, `toEquiv`, `trans`, `ulift`, `«term_≃ᵐ_»`	49
Theorems `of_union_range_cover`, `of_union₃_range_cover`, `comap_eq`, `comp`, `equivRange_apply`, `equivRange_symm_apply_mk`, `exists_measurable_extend`, `id`, `iff_comap_eq`, `injective`, `leftInverse_invFun`, `measurable`, `measurableSet_image`, `measurableSet_image'`, `measurableSet_preimage`, `measurableSet_range`, `measurable_comp_iff`, `measurable_extend`, `measurable_invFun`, `measurable_rangeSplitting`, `of_measurable_inverse`, `of_measurable_inverse_on_range`, `subtype_coe`, `apply_symm_apply`, `bijective`, `coe_curry`, `coe_curry_symm`, `coe_mk`, `coe_piCongrLeft`, `coe_piCurry`, `coe_piCurry_symm`, `coe_setOf`, `coe_sumPiEquivProdPi`, `coe_sumPiEquivProdPi_symm`, `coe_toEquiv`, `coe_toEquiv_symm`, `coe_trans`, `curry_apply`, `curry_symm_apply`, `eq_image_iff_symm_image_eq`, `ext`, `ext_iff`, `finTwoArrow_apply`, `finTwoArrow_symm_apply`, `funUnique_apply`, `funUnique_symm_apply`, `image_eq_preimage_symm`, `image_preimage`, `image_symm`, `injective`, `map_eq`, `measurable`, `measurableEmbedding`, `measurableSet_image`, `measurableSet_preimage`, `measurable_comp_iff`, `measurable_invFun`, `measurable_toFun`, `ofInvolutive_apply`, `ofInvolutive_symm`, `ofInvolutive_toEquiv`, `piCongrLeft_apply_apply`, `piCurry_apply`, `piCurry_symm_apply`, `piEquivPiSubtypeProd_apply`, `piEquivPiSubtypeProd_symm_apply`, `piFinSuccAbove_apply`, `piFinSuccAbove_symm_apply`, `piFinTwo_apply`, `piFinTwo_symm_apply`, `piMeasurableEquivTProd_apply`, `piMeasurableEquivTProd_symm_apply`, `piUnique_apply`, `piUnique_symm_apply`, `preimage_image`, `preimage_symm`, `refl_apply`, `refl_toEquiv`, `self_comp_symm`, `self_trans_symm`, `setOf_apply`, `setOf_symm_apply`, `surjective`, `symm_apply_apply`, `symm_bijective`, `symm_comp_self`, `symm_mk`, `symm_preimage_preimage`, `symm_refl`, `symm_symm`, `symm_trans_self`, `toEquiv_injective`, `trans_apply`, `trans_toEquiv`, `exists_measurable_proj`, `of_union_range_cover`, `of_union₃_range_cover`, `comap_compl`, `comap_not`	99
Total	148

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_union_range_cover` 📖	—	`MeasurableEmbedding` `Set` `Set.instHasSubset` `Set.univ` `Set.instUnion` `Set.range` `Measurable`	—	—	`MeasurableSet.of_union_range_cover`
`of_union₃_range_cover` 📖	—	`MeasurableEmbedding` `Set` `Set.instHasSubset` `Set.univ` `Set.instUnion` `Set.range` `Measurable`	—	—	`MeasurableSet.of_union₃_range_cover`

MeasurableEmbedding

Definitions

Name	Category	Theorems
`equivImage` 📖	CompOp	—
`equivRange` 📖	CompOp	2 math math: `equivRange_apply`, `equivRange_symm_apply_mk`
`invFun` 📖	CompOp	2 math math: `leftInverse_invFun`, `measurable_invFun`
`schroederBernstein` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eq` 📖	mathematical	`MeasurableEmbedding`	`MeasurableSpace.comap`	—	`LE.le.antisymm` `Measurable.comap_le` `measurable` `measurableSet_image'` `Function.Injective.preimage_image` `injective`
`comp` 📖	—	`MeasurableEmbedding`	—	—	`injective` `Measurable.comp` `measurable` `Set.image_comp` `measurableSet_image`
`equivRange_apply` 📖	mathematical	`MeasurableEmbedding`	`DFunLike.coe` `MeasurableEquiv` `Set.Elem` `Set.range` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `equivRange` `Set.mem_range_self`	—	`Set.mem_range_self` `Set.image_univ` `set_coe_cast`
`equivRange_symm_apply_mk` 📖	mathematical	`MeasurableEmbedding`	`DFunLike.coe` `MeasurableEquiv` `Set.Elem` `Set.range` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `equivRange` `Set.mem_range_self`	—	`Set.mem_range_self` `MeasurableEquiv.symm_apply_apply` `equivRange_apply`
`exists_measurable_extend` 📖	—	`MeasurableEmbedding` `Measurable`	—	—	`measurable_extend` `measurable_const'` `Function.Injective.extend_apply` `injective`
`id` 📖	mathematical	—	`MeasurableEmbedding`	—	`measurable_id` `Set.image_id`
`iff_comap_eq` 📖	mathematical	—	`MeasurableEmbedding` `MeasurableSpace.comap` `MeasurableSet` `Set.range`	—	`injective` `comap_eq` `measurableSet_range` `comap_measurable` `Set.image_preimage_eq_inter_range` `MeasurableSet.inter`
`injective` 📖	—	`MeasurableEmbedding`	—	—	—
`leftInverse_invFun` 📖	mathematical	`MeasurableEmbedding`	`invFun`	—	—
`measurable` 📖	mathematical	`MeasurableEmbedding`	`Measurable`	—	—
`measurableSet_image` 📖	mathematical	`MeasurableEmbedding`	`MeasurableSet` `Set.image`	—	`Function.Injective.preimage_image` `injective` `measurable` `measurableSet_image'`
`measurableSet_image'` 📖	mathematical	`MeasurableEmbedding` `MeasurableSet`	`Set.image`	—	—
`measurableSet_preimage` 📖	mathematical	`MeasurableEmbedding`	`MeasurableSet` `Set.preimage` `Set` `Set.instInter` `Set.range`	—	`Set.image_preimage_eq_inter_range` `measurableSet_image`
`measurableSet_range` 📖	mathematical	`MeasurableEmbedding`	`MeasurableSet` `Set.range`	—	`Set.image_univ` `measurableSet_image'` `MeasurableSet.univ`
`measurable_comp_iff` 📖	mathematical	`MeasurableEmbedding`	`Measurable`	—	`Measurable.comp` `measurable_rangeSplitting` `Set.mem_range_self` `Function.RightInverse.comp_eq_id` `Set.rightInverse_rangeSplitting` `injective` `measurable`
`measurable_extend` 📖	mathematical	`MeasurableEmbedding` `Measurable`	`Function.extend`	—	`measurable_of_restrict_of_restrict_compl` `measurableSet_range` `Subtype.coe_prop` `Set.restrict_extend_range` `Measurable.comp` `measurable_rangeSplitting` `Set.restrict_extend_compl_range` `measurable_subtype_coe`
`measurable_invFun` 📖	mathematical	`MeasurableEmbedding`	`Measurable` `invFun`	—	`Measurable.dite` `MeasurableEquiv.measurable` `measurable_const` `measurableSet_range`
`measurable_rangeSplitting` 📖	mathematical	`MeasurableEmbedding`	`Measurable` `Set.Elem` `Set.range` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Set.rangeSplitting`	—	`Set.preimage_rangeSplitting` `injective` `measurableSet_image` `subtype_coe` `measurableSet_range` `Set.image_comp` `Set.coe_comp_rangeFactorization`
`of_measurable_inverse` 📖	mathematical	`Measurable` `MeasurableSet` `Set.range`	`MeasurableEmbedding`	—	`of_measurable_inverse_on_range` `Measurable.comp` `measurable_subtype_coe`
`of_measurable_inverse_on_range` 📖	mathematical	`Measurable` `MeasurableSet` `Set.range` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Set.rangeFactorization`	`MeasurableEmbedding`	—	`Function.LeftInverse.rightInverse_of_surjective` `Set.rangeFactorization_surjective` `Set.mem_range_self` `comp` `subtype_coe` `MeasurableEquiv.measurableEmbedding`
`subtype_coe` 📖	mathematical	`MeasurableSet`	`MeasurableEmbedding` `Set` `Set.instMembership` `Subtype.instMeasurableSpace`	—	`Subtype.coe_injective` `measurable_subtype_coe` `MeasurableSet.subtype_image`

MeasurableEquiv

Definitions

Name	Category	Theorems
`arrowCongr'` 📖	CompOp	2 math math: `MeasureTheory.volume_preserving_arrowCongr'`, `MeasureTheory.measurePreserving_arrowCongr'`
`arrowProdEquivProdArrow` 📖	CompOp	2 math math: `MeasureTheory.measurePreserving_arrowProdEquivProdArrow`, `MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow`
`cast` 📖	CompOp	—
`curry` 📖	CompOp	6 math math: `curry_symm_apply`, `curry_apply`, `MeasureTheory.Measure.infinitePi_map_curry_symm`, `coe_curry_symm`, `coe_curry`, `MeasureTheory.Measure.infinitePi_map_curry`
`finTwoArrow` 📖	CompOp	5 math math: `finTwoArrow_apply`, `MeasureTheory.measurePreserving_finTwoArrow_vec`, `finTwoArrow_symm_apply`, `MeasureTheory.volume_preserving_finTwoArrow`, `MeasureTheory.measurePreserving_finTwoArrow`
`funUnique` 📖	CompOp	5 math math: `MeasureTheory.measurePreserving_funUnique`, `funUnique_symm_apply`, `funUnique_apply`, `MeasureTheory.hausdorffMeasure_measurePreserving_funUnique`, `MeasureTheory.volume_preserving_funUnique`
`instEquivLike` 📖	CompOp	170 math math: `injective`, `piCurry_apply`, `surjective`, `preimage_symm`, `smul_apply`, `coe_smul₀`, `measurableEmbedding`, `bijective`, `MeasureTheory.measurePreserving_funUnique`, `ProbabilityTheory.Kernel.partialTraj_succ_of_le`, `map_apply`, `MeasureTheory.volume_measurePreserving_piCongrLeft`, `image_preimage`, `unitInterval.coe_symmMeasurableEquiv`, `MeasureTheory.Measure.pi_map_piCongrLeft`, `preimage_image`, `finTwoArrow_apply`, `trans_apply`, `piFinTwo_symm_apply`, `MeasureTheory.volume_preserving_piFinsetUnion`, `Complex.measurableEquivPi_apply`, `unitInterval.symmMeasurableEquiv_apply`, `self_comp_symm`, `MeasureTheory.measurePreserving_finTwoArrow_vec`, `comap_apply`, `toLp_symm_apply`, `funUnique_symm_apply`, `coe_toEquiv`, `coe_sumPiEquivProdPi`, `piEquivPiSubtypeProd_apply`, `MeasureTheory.Measure.infinitePi_map_piCongrLeft`, `MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo`, `Complex.measurableEquivRealProd_apply`, `MeasureTheory.Measure.infinitePi_map_piCurry`, `map_symm_map`, `MeasureTheory.volume_preserving_prodAssoc`, `quasiMeasurePreserving_symm`, `ofInvolutive_apply`, `MeasureTheory.IsProbabilityMeasure_comap_equiv`, `coe_IicProdIoc_symm`, `ProbabilityTheory.variance_map_equiv`, `symm_preimage_preimage`, `MeasureTheory.Measure.map_piSingleton`, `MeasureTheory.integrable_map_equiv`, `MeasureTheory.volume_preserving_piFinSuccAbove`, `restrict_map`, `LinearIsometryEquiv.coe_toMeasurableEquiv`, `measurableSet_image`, `MeasureTheory.Measure.compProd_assoc'`, `MeasurableEmbedding.equivRange_apply`, `MeasureTheory.measurePreserving_piCongrLeft`, `MeasureTheory.setIntegral_map_equiv`, `neg_apply`, `MeasureTheory.measurePreserving_arrowProdEquivProdArrow`, `coe_mk`, `map_apply_eq_iff_map_symm_apply_eq`, `coe_toLp`, `ProbabilityTheory.Kernel.partialTraj_le_def`, `MeasureTheory.volume_preserving_pi_empty`, `ext_iff`, `MeasureTheory.integral_map_equiv`, `ProbabilityTheory.Kernel.prodAssoc_symm_prod`, `comap_symm`, `MeasureTheory.Measure.infinitePiNat_map_piCongrLeft`, `MeasureTheory.measurePreserving_piFinTwo`, `curry_symm_apply`, `ProbabilityTheory.Kernel.prodAssoc_prod`, `MeasureTheory.measurePreserving_prodAssoc`, `memLp_map_measure_iff`, `unitInterval.symmMeasurableEquiv_symm_apply`, `curry_apply`, `ProbabilityTheory.Kernel.partialTraj_succ_self`, `apply_symm_apply`, `sigmaFinite_map`, `MeasureTheory.measurePreserving_piFinSuccAbove`, `piUnique_symm_apply`, `piUnique_apply`, `NumberField.mixedEmbedding.fundamentalDomain_stdBasis`, `piCongrLeft_apply_apply`, `coe_IicProdIoc`, `Complex.measurableEquivRealProd_symm_polarCoord_symm_apply`, `Complex.volume_preserving_equiv_real_prod`, `coe_piCongrLeft`, `funUnique_apply`, `refl_apply`, `MeasureTheory.measurePreserving_piUnique`, `MeasureTheory.Measure.infinitePi_map_curry_symm`, `MeasureTheory.hausdorffMeasure_measurePreserving_funUnique`, `MeasureTheory.integrableOn_map_equiv`, `piEquivPiSubtypeProd_symm_apply`, `ProbabilityTheory.Kernel.prodComm_prod`, `map_map_symm`, `symm_apply_apply`, `MeasureTheory.volume_preserving_piFinTwo`, `Complex.measurableEquivPi_symm_apply`, `ProbabilityTheory.covariance_map_equiv`, `image_symm`, `piMeasurableEquivTProd_apply`, `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, `vadd_apply`, `Complex.volume_preserving_equiv_pi`, `MeasureTheory.Measure.compProd_assoc`, `piCurry_symm_apply`, `coe_curry_symm`, `coe_sumPiEquivProdPi_symm`, `measurable_comp_iff`, `image_eq_preimage_symm`, `inv_apply`, `coe_addLeft`, `finTwoArrow_symm_apply`, `MeasurableEmbedding.equivRange_symm_apply_mk`, `Homeomorph.toMeasurableEquiv_symm_coe`, `MeasureTheory.measurePreserving_piFinsetUnion`, `aemeasurable_map_equiv_iff`, `MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow`, `coe_setOf`, `measurableSet_preimage`, `symm_comp_self`, `ProbabilityTheory.Kernel.compProd_assoc`, `ProbabilityTheory.Kernel.compProd_def`, `coe_toEquiv_symm`, `MeasureTheory.volume_preserving_piUnique`, `coe_addRight`, `coe_mulRight`, `piFinTwo_apply`, `map_measurableEquiv_injective`, `setOf_symm_apply`, `coe_piCurry`, `measurable`, `coe_mulLeft₀`, `MeasureTheory.Measure.prodAssoc_prod`, `EuclideanSpace.coe_measurableEquiv`, `MeasureTheory.measurePreserving_sumPiEquivProdPi_symm`, `coe_piCurry_symm`, `coe_trans`, `MeasureTheory.measurePreserving_piEquivPiSubtypeProd`, `map_eq`, `MeasureTheory.volume_preserving_finTwoArrow`, `MeasureTheory.Measure.pi_map_piOptionEquivProd`, `MeasureTheory.measurePreserving_pi_empty`, `Ergodic.symm_iff`, `eq_image_iff_symm_image_eq`, `coe_mulLeft`, `MeasureTheory.lintegral_map_equiv`, `Complex.measurableEquivRealProd_symm_apply`, `MeasureTheory.measurePreserving_finTwoArrow`, `OrthonormalBasis.measurePreserving_measurableEquiv`, `setOf_apply`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi`, `map_ae`, `MeasureTheory.volume_preserving_piEquivPiSubtypeProd`, `toLp_apply`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm`, `MeasureTheory.Measure.infinitePi_map_piCurry_symm`, `MeasureTheory.volume_preserving_funUnique`, `EuclideanSpace.coe_measurableEquiv_symm`, `map_symm`, `MeasureTheory.measurePreserving_sumPiEquivProdPi`, `ProbabilityTheory.Kernel.map_apply_eq_iff_map_symm_apply_eq`, `coe_curry`, `MeasureTheory.Measure.infinitePi_map_curry`, `coe_mulRight₀`, `MeasureTheory.MeasurableEquiv.measurePreserving_symm`, `coe_toLp_symm`, `piMeasurableEquivTProd_symm_apply`, `piFinSuccAbove_symm_apply`, `Homeomorph.toMeasurableEquiv_coe`, `ProbabilityTheory.Kernel.traj_eq_prod`, `piFinSuccAbove_apply`, `LinearIsometryEquiv.coe_symm_toMeasurableEquiv`
`instInhabited` 📖	CompOp	—
`ofInvolutive` 📖	CompOp	3 math math: `ofInvolutive_toEquiv`, `ofInvolutive_apply`, `ofInvolutive_symm`
`ofUniqueOfUnique` 📖	CompOp	2 math math: `MeasureTheory.volume_preserving_pi_empty`, `MeasureTheory.measurePreserving_pi_empty`
`piCongrLeft` 📖	CompOp	7 math math: `MeasureTheory.volume_measurePreserving_piCongrLeft`, `MeasureTheory.Measure.pi_map_piCongrLeft`, `MeasureTheory.Measure.infinitePi_map_piCongrLeft`, `MeasureTheory.measurePreserving_piCongrLeft`, `MeasureTheory.Measure.infinitePiNat_map_piCongrLeft`, `piCongrLeft_apply_apply`, `coe_piCongrLeft`
`piCongrRight` 📖	CompOp	—
`piCurry` 📖	CompOp	6 math math: `piCurry_apply`, `MeasureTheory.Measure.infinitePi_map_piCurry`, `piCurry_symm_apply`, `coe_piCurry`, `coe_piCurry_symm`, `MeasureTheory.Measure.infinitePi_map_piCurry_symm`
`piEquivPiSubtypeProd` 📖	CompOp	4 math math: `piEquivPiSubtypeProd_apply`, `piEquivPiSubtypeProd_symm_apply`, `MeasureTheory.measurePreserving_piEquivPiSubtypeProd`, `MeasureTheory.volume_preserving_piEquivPiSubtypeProd`
`piFinSuccAbove` 📖	CompOp	4 math math: `MeasureTheory.volume_preserving_piFinSuccAbove`, `MeasureTheory.measurePreserving_piFinSuccAbove`, `piFinSuccAbove_symm_apply`, `piFinSuccAbove_apply`
`piFinTwo` 📖	CompOp	5 math math: `piFinTwo_symm_apply`, `MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo`, `MeasureTheory.measurePreserving_piFinTwo`, `MeasureTheory.volume_preserving_piFinTwo`, `piFinTwo_apply`
`piFinsetUnion` 📖	CompOp	2 math math: `MeasureTheory.volume_preserving_piFinsetUnion`, `MeasureTheory.measurePreserving_piFinsetUnion`
`piMeasurableEquivTProd` 📖	CompOp	2 math math: `piMeasurableEquivTProd_apply`, `piMeasurableEquivTProd_symm_apply`
`piOptionEquivProd` 📖	CompOp	1 math math: `MeasureTheory.Measure.pi_map_piOptionEquivProd`
`piUnique` 📖	CompOp	4 math math: `piUnique_symm_apply`, `piUnique_apply`, `MeasureTheory.measurePreserving_piUnique`, `MeasureTheory.volume_preserving_piUnique`
`prodAssoc` 📖	CompOp	9 math math: `MeasureTheory.volume_preserving_prodAssoc`, `MeasureTheory.Measure.compProd_assoc'`, `ProbabilityTheory.Kernel.prodAssoc_symm_prod`, `ProbabilityTheory.Kernel.prodAssoc_prod`, `MeasureTheory.measurePreserving_prodAssoc`, `MeasureTheory.Measure.compProd_assoc`, `ProbabilityTheory.Kernel.compProd_assoc`, `ProbabilityTheory.Kernel.compProd_def`, `MeasureTheory.Measure.prodAssoc_prod`
`prodComm` 📖	CompOp	1 math math: `ProbabilityTheory.Kernel.prodComm_prod`
`prodCongr` 📖	CompOp	—
`prodPUnit` 📖	CompOp	—
`prodSumDistrib` 📖	CompOp	—
`punitProd` 📖	CompOp	—
`refl` 📖	CompOp	5 math math: `refl_toEquiv`, `refl_apply`, `symm_trans_self`, `symm_refl`, `self_trans_symm`
`setOf` 📖	CompOp	3 math math: `coe_setOf`, `setOf_symm_apply`, `setOf_apply`
`sumCompl` 📖	CompOp	—
`sumCongr` 📖	CompOp	—
`sumPiEquivProdPi` 📖	CompOp	6 math math: `coe_sumPiEquivProdPi`, `coe_sumPiEquivProdPi_symm`, `MeasureTheory.measurePreserving_sumPiEquivProdPi_symm`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm`, `MeasureTheory.measurePreserving_sumPiEquivProdPi`
`sumProdDistrib` 📖	CompOp	—
`sumProdSum` 📖	CompOp	—
`toEquiv` 📖	CompOp	19 math math: `toEquiv_mulLeft`, `toEquiv_mulRight₀`, `smul_toEquiv`, `ofInvolutive_toEquiv`, `toEquiv_mulRight`, `refl_toEquiv`, `coe_toEquiv`, `toEquiv_addRight`, `neg_toEquiv`, `toEquiv_addLeft`, `toEquiv_injective`, `measurable_toFun`, `measurable_invFun`, `trans_toEquiv`, `coe_toEquiv_symm`, `inv_toEquiv`, `vadd_toEquiv`, `EuclideanSpace.measurableEquiv_toEquiv`, `toEquiv_mulLeft₀`
`trans` 📖	CompOp	6 math math: `trans_apply`, `trans_toEquiv`, `symm_trans_self`, `self_trans_symm`, `coe_trans`, `MeasureTheory.MeasurePreserving.trans`
`ulift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.right_inv`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.bijective`
`coe_curry` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `curry`	—	—
`coe_curry_symm` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `curry`	—	—
`coe_mk` 📖	mathematical	`Measurable` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	`MeasurableEquiv` `instEquivLike`	—	—
`coe_piCongrLeft` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft` `Equiv.piCongrLeft`	—	—
`coe_piCurry` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `piCurry` `Sigma.curry`	—	—
`coe_piCurry_symm` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `piCurry` `Sigma.uncurry`	—	—
`coe_setOf` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Set` `MeasurableSpace.pi` `Prop.instMeasurableSpace` `Set.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `setOf` `setOf`	—	—
`coe_sumPiEquivProdPi` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `sumPiEquivProdPi` `Equiv` `Equiv.instEquivLike` `Equiv.sumPiEquivProdPi`	—	—
`coe_sumPiEquivProdPi_symm` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `sumPiEquivProdPi` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `Equiv.sumPiEquivProdPi`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `MeasurableEquiv` `instEquivLike`	—	—
`coe_toEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `MeasurableEquiv` `instEquivLike` `symm`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`curry_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `curry`	—	—
`curry_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `curry`	—	—
`eq_image_iff_symm_image_eq` 📖	mathematical	—	`Set.image` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`coe_toEquiv` `Equiv.eq_image_iff_symm_image_eq` `coe_toEquiv_symm`
`ext` 📖	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext'`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`finTwoArrow_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `finTwoArrow`	—	—
`finTwoArrow_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `finTwoArrow` `Fin.cons` `finZeroElim`	—	—
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `funUnique` `Unique.instInhabited`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `funUnique` `uniqueElim`	—	—
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.preimage` `symm`	—	`Equiv.image_eq_preimage_symm`
`image_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.preimage`	—	`coe_toEquiv` `Equiv.image_preimage`
`image_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.preimage`	—	`Equiv.image_symm_eq_preimage`
`injective` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.injective`
`map_eq` 📖	mathematical	—	`MeasurableSpace.map` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`LE.le.antisymm'` `Measurable.le_map` `measurable` `measurableSet_preimage`
`measurable` 📖	mathematical	—	`Measurable` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`measurable_toFun`
`measurableEmbedding` 📖	mathematical	—	`MeasurableEmbedding` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`injective` `measurable` `measurableSet_image`
`measurableSet_image` 📖	mathematical	—	`MeasurableSet` `Set.image` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`image_eq_preimage_symm` `measurableSet_preimage`
`measurableSet_preimage` 📖	mathematical	—	`MeasurableSet` `Set.preimage` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`symm_preimage_preimage` `measurable`
`measurable_comp_iff` 📖	mathematical	—	`Measurable` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Measurable.comp` `measurable` `symm_trans_self` `coe_toEquiv`
`measurable_invFun` 📖	mathematical	—	`Measurable` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv`	—	—
`measurable_toFun` 📖	mathematical	—	`Measurable` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv`	—	—
`ofInvolutive_apply` 📖	mathematical	`Function.Involutive` `Measurable`	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `ofInvolutive`	—	—
`ofInvolutive_symm` 📖	mathematical	`Function.Involutive` `Measurable`	`symm` `ofInvolutive`	—	—
`ofInvolutive_toEquiv` 📖	mathematical	`Function.Involutive` `Measurable`	`toEquiv` `ofInvolutive` `Function.Involutive.toPerm`	—	—
`piCongrLeft_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft`	—	`piCongrLeft.eq_1` `Equiv.piCongrLeft_apply_apply`
`piCurry_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `piCurry` `Sigma.curry`	—	—
`piCurry_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `piCurry` `Sigma.uncurry`	—	—
`piEquivPiSubtypeProd_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `piEquivPiSubtypeProd`	—	—
`piEquivPiSubtypeProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `piEquivPiSubtypeProd`	—	—
`piFinSuccAbove_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `Fin.succAbove` `EquivLike.toFunLike` `instEquivLike` `piFinSuccAbove` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `Fin.insertNthEquiv`	—	—
`piFinSuccAbove_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `Fin.succAbove` `EquivLike.toFunLike` `instEquivLike` `symm` `piFinSuccAbove` `Equiv` `Equiv.instEquivLike` `Fin.insertNthEquiv`	—	—
`piFinTwo_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `piFinTwo`	—	—
`piFinTwo_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `piFinTwo` `Fin.cons` `finZeroElim`	—	—
`piMeasurableEquivTProd_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `List.TProd` `MeasurableSpace.pi` `TProd.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `piMeasurableEquivTProd`	—	—
`piMeasurableEquivTProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `List.TProd` `TProd.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `piMeasurableEquivTProd` `List.TProd.elim'`	—	—
`piUnique_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Unique.instInhabited` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `piUnique`	—	—
`piUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Unique.instInhabited` `MeasurableSpace.pi` `EquivLike.toFunLike` `instEquivLike` `symm` `piUnique` `uniqueElim`	—	—
`preimage_image` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.image`	—	`coe_toEquiv` `Equiv.preimage_image`
`preimage_symm` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.image`	—	`image_eq_preimage_symm`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`refl_toEquiv` 📖	mathematical	—	`toEquiv` `refl` `Equiv.refl`	—	—
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.right_inv`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_comp_self`
`setOf_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Set` `MeasurableSpace.pi` `Prop.instMeasurableSpace` `Set.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `setOf` `setOf`	—	—
`setOf_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Set` `Set.instMeasurableSpace` `MeasurableSpace.pi` `Prop.instMeasurableSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `setOf` `Set.instMembership`	—	—
`surjective` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.left_inv`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `MeasurableEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.left_inv`
`symm_mk` 📖	mathematical	`Measurable` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	`symm`	—	—
`symm_preimage_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_preimage_preimage`
`symm_refl` 📖	mathematical	—	`symm` `refl`	—	—
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `self_comp_symm`
`toEquiv_injective` 📖	mathematical	—	`MeasurableEquiv` `Equiv` `toEquiv`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_toEquiv` 📖	mathematical	—	`toEquiv` `trans` `Equiv.trans`	—	—

MeasurableEquiv.Set

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	—
`rangeInl` 📖	CompOp	—
`rangeInr` 📖	CompOp	—
`singleton` 📖	CompOp	—
`univ` 📖	CompOp	—

MeasurableEquiv.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_measurable_proj` 📖	mathematical	`MeasurableSet` `Set.Nonempty`	`Measurable` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership`	—	`MeasurableEmbedding.exists_measurable_extend` `MeasurableEmbedding.subtype_coe` `measurable_id` `Set.Nonempty.to_subtype`
`of_union_range_cover` 📖	—	`MeasurableEmbedding` `Set` `Set.instHasSubset` `Set.univ` `Set.instUnion` `Set.range` `MeasurableSet` `Set.preimage`	—	—	`Set.image_preimage_eq_range_inter` `Set.univ_subset_iff` `Set.univ_inter` `union` `MeasurableEmbedding.measurableSet_image'`
`of_union₃_range_cover` 📖	—	`MeasurableEmbedding` `Set` `Set.instHasSubset` `Set.univ` `Set.instUnion` `Set.range` `MeasurableSet` `Set.preimage`	—	—	`Set.image_preimage_eq_range_inter` `Set.univ_subset_iff` `Set.univ_inter` `union` `MeasurableEmbedding.measurableSet_image'`

MeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_compl` 📖	mathematical	`Measurable` `Compl.compl` `BooleanAlgebra.toCompl`	`comap` `MeasurableSpace`	—	`comap_comp` `MeasurableEmbedding.comap_eq` `compl_involutive` `MeasurableEquiv.measurableEmbedding`
`comap_not` 📖	mathematical	—	`comap` `MeasurableSpace` `Prop.instMeasurableSpace`	—	`comap_compl` `measurableSet_top`

(root)

Definitions

Name	Category	Theorems
`MeasurableEmbedding` 📖	CompData	37 math math: `MeasurableEquiv.measurableEmbedding`, `Continuous.measurableEmbedding`, `measurableEmbedding_mulRight₀`, `MeasureTheory.measurableEmbedding_embeddingReal`, `Homeomorph.measurableEmbedding`, `measurableEmbedding_subLeft`, `measurableEmbedding_const_smul₀`, `measurableEmbedding_divLeft`, `measurableEmbedding_sigmoid`, `measurableEmbedding_divRight`, `measurableEmbedding_sigmoid_comp_embeddingReal`, `MeasureTheory.measurableEmbedding_of_fderivWithin`, `MeasurableEmbedding.id`, `measurableEmbedding_subRight`, `measurableEmbedding_const_smul`, `measurableEmbedding_const_vadd`, `ContinuousOn.measurableEmbedding`, `measurableEmbedding_addRight`, `measurableEmbedding_mulLeft`, `MeasurableEmbedding.of_measurable_inverse_on_range`, `MeasurableEmbedding.of_measurable_inverse`, `measurableEmbedding_neg`, `Topology.IsOpenEmbedding.measurableEmbedding`, `MeasureTheory.exists_measurableEmbedding_real`, `measurableEmbedding_inv`, `Measurable.measurableEmbedding`, `Topology.IsClosedEmbedding.measurableEmbedding`, `unitInterval.measurableEmbedding_coe`, `MeasurableEmbedding.iff_comap_eq`, `measurableEmbedding_prodMk_left`, `measurableEmbedding_prod_mk_right`, `EReal.measurableEmbedding_coe`, `measurableEmbedding_addLeft`, `measurableEmbedding_mulRight`, `Topology.IsEmbedding.measurableEmbedding`, `MeasurableEmbedding.subtype_coe`, `measurableEmbedding_mulLeft₀`
`«term_≃ᵐ_»` 📖	CompOp	—

---

← Back to Index