ProdLp

📁 Source: Mathlib/Analysis/Normed/Lp/ProdLp.lean

Statistics

Metric	Count
Definitions `withLpProdAssoc`, `withLpProdComm`, `withLpProdCongr`, `withLpProdUnique`, `withLpUniqueProd`, `withLpProdCongr`, `withLpProdMap`, `withLpProdAssoc`, `withLpProdComm`, `withLpProdCongr`, `withLpProdUnique`, `withLpUniqueProd`, `fst`, `fstL`, `fstₗ`, `homeomorphProd`, `idemFst`, `idemSnd`, `instProdBornology`, `instProdDist`, `instProdEDist`, `instProdEMetricSpace`, `instProdMetricSpace`, `instProdNorm`, `instProdNormedAddCommGroup`, `instProdNormedSpace`, `instProdPseudoEMetricSpace`, `instProdPseudoMetricSpace`, `instProdSeminormedAddCommGroup`, `instProdTopologicalSpace`, `instProdUniformSpace`, `normedAddCommGroupToProd`, `normedSpaceSeminormedAddCommGroupToProd`, `prodContinuousLinearEquiv`, `prodEquivₗᵢ`, `prodPseudoEMetricAux`, `prodPseudoMetricAux`, `pseudoMetricSpaceToProd`, `seminormedAddCommGroupToProd`, `snd`, `sndL`, `sndₗ`, `uniformEquivProd`	43
Theorems `withLpProdMap`, `coe_withLpProdUnique`, `coe_withLpUniqueProd`, `withLpProdAssoc_apply`, `withLpProdAssoc_symm_apply`, `withLpProdComm_apply`, `withLpProdComm_symm`, `withLpProdCongr_apply`, `withLpProdCongr_symm_apply`, `withLpProdUnique_apply`, `withLpProdUnique_symm_apply`, `withLpUniqueProd_apply`, `withLpUniqueProd_symm_apply`, `withLpProdMap_apply`, `coe_withLpProdUnique`, `coe_withLpUniqueProd`, `withLpProdAssoc_apply`, `withLpProdAssoc_symm_apply`, `withLpProdComm_apply`, `withLpProdComm_symm`, `withLpProdCongr_apply`, `withLpProdCongr_symm_apply`, `withLpProdUnique_apply`, `withLpProdUnique_symm_apply`, `withLpUniqueProd_apply`, `withLpUniqueProd_symm_apply`, `add_fst`, `add_snd`, `coe_fstL`, `coe_sndL`, `continuous_fst`, `continuous_snd`, `dist_fst_le`, `dist_pseudoMetricSpaceToProd`, `dist_snd_le`, `dist_toLp_fst`, `dist_toLp_snd`, `edist_fst_le`, `edist_snd_le`, `edist_toLp_fst`, `edist_toLp_snd`, `enorm_fst_le`, `enorm_snd_le`, `fstL_apply`, `fstₗ_apply`, `idemFst_add_idemSnd`, `idemFst_apply`, `idemFst_compl`, `idemSnd_apply`, `idemSnd_compl`, `instProdCompleteSpace`, `instProdIsBoundedSMul`, `instProdNormSMulClass`, `instProdT0Space`, `isBoundedSMulSeminormedAddCommGroupToProd`, `isUniformInducing_toLp`, `neg_fst`, `neg_snd`, `nndist_fst_le`, `nndist_snd_le`, `nndist_toLp_fst`, `nndist_toLp_snd`, `nnnorm_fst_le`, `nnnorm_seminormedAddCommGroupToProd`, `nnnorm_snd_le`, `nnnorm_toLp_inl`, `nnnorm_toLp_inr`, `normSMulClassSeminormedAddCommGroupToProd`, `norm_fst_le`, `norm_seminormedAddCommGroupToProd`, `norm_snd_le`, `norm_toLp_fst`, `norm_toLp_snd`, `ofLp_fst`, `ofLp_snd`, `prodContinuousLinearEquiv_apply`, `prodContinuousLinearEquiv_symm_apply`, `prodContinuousLinearEquiv_symm_apply_ofLp`, `prod_antilipschitzWith_ofLp`, `prod_antilipschitzWith_toLp`, `prod_continuous_ofLp`, `prod_continuous_toLp`, `prod_dist_eq_add`, `prod_dist_eq_card`, `prod_dist_eq_of_L1`, `prod_dist_eq_of_L2`, `prod_dist_eq_sup`, `prod_edist_comm`, `prod_edist_eq_add`, `prod_edist_eq_card`, `prod_edist_eq_of_L1`, `prod_edist_eq_of_L2`, `prod_edist_eq_sup`, `prod_edist_self`, `prod_isometry_ofLp_infty`, `prod_lipschitzWith_ofLp`, `prod_lipschitzWith_toLp`, `prod_nndist_eq_add`, `prod_nndist_eq_of_L1`, `prod_nndist_eq_of_L2`, `prod_nndist_eq_sup`, `prod_nnnorm_eq_add`, `prod_nnnorm_eq_of_L1`, `prod_nnnorm_eq_of_L2`, `prod_nnnorm_eq_sup`, `prod_nnnorm_ofLp`, `prod_nnnorm_toLp`, `prod_norm_eq_add`, `prod_norm_eq_add_idemFst`, `prod_norm_eq_card`, `prod_norm_eq_idemFst_of_L1`, `prod_norm_eq_idemFst_sup_idemSnd`, `prod_norm_eq_of_L1`, `prod_norm_eq_of_L2`, `prod_norm_eq_of_nat`, `prod_norm_eq_sup`, `prod_norm_ofLp`, `prod_norm_sq_eq_of_L2`, `prod_norm_toLp`, `prod_sup_edist_ne_top_aux`, `prod_uniformContinuous_ofLp`, `prod_uniformContinuous_toLp`, `secondCountableTopology`, `smul_fst`, `smul_snd`, `sndL_apply`, `sndₗ_apply`, `sub_fst`, `sub_snd`, `toEquiv_homeomorphProd`, `toEquiv_uniformEquivProd`, `toHomeomorph_uniformEquivProd`, `toLp_fst`, `toLp_snd`, `zero_fst`, `zero_snd`	136
Total	179

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withLpProdMap` 📖	mathematical	`Isometry`	`WithLp` `WithLp.instProdPseudoEMetricSpace` `WithLp.map`	—	`ENNReal.trichotomy` `Fact.elim` `ENNReal.instCanonicallyOrderedAdd` `NeZero.charZero_one` `ENNReal.instCharZero` `edist_eq` `WithLp.prod_edist_eq_add` `one_div`

IsometryEquiv

Definitions

Name	Category	Theorems
`withLpProdAssoc` 📖	CompOp	2 math math: `withLpProdAssoc_apply`, `withLpProdAssoc_symm_apply`
`withLpProdComm` 📖	CompOp	2 math math: `withLpProdComm_symm`, `withLpProdComm_apply`
`withLpProdCongr` 📖	CompOp	2 math math: `withLpProdCongr_apply`, `withLpProdCongr_symm_apply`
`withLpProdUnique` 📖	CompOp	3 math math: `withLpProdUnique_apply`, `coe_withLpProdUnique`, `withLpProdUnique_symm_apply`
`withLpUniqueProd` 📖	CompOp	3 math math: `withLpUniqueProd_symm_apply`, `coe_withLpUniqueProd`, `withLpUniqueProd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_withLpProdUnique` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpProdUnique` `WithLp.fst`	—	—
`coe_withLpUniqueProd` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpUniqueProd` `WithLp.snd`	—	—
`withLpProdAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpProdAssoc` `WithLp.toLp` `WithLp.fst` `WithLp.snd`	—	—
`withLpProdAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpProdAssoc` `WithLp.toLp` `WithLp.fst` `WithLp.snd`	—	—
`withLpProdComm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpProdComm` `WithLp.toLp` `WithLp.snd` `WithLp.fst`	—	—
`withLpProdComm_symm` 📖	mathematical	—	`symm` `WithLp` `WithLp.instProdPseudoEMetricSpace` `withLpProdComm`	—	—
`withLpProdCongr_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpProdCongr` `WithLp.toLp` `WithLp.ofLp`	—	—
`withLpProdCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpProdCongr` `WithLp.toLp` `WithLp.ofLp`	—	—
`withLpProdUnique_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpProdUnique` `WithLp.fst`	—	—
`withLpProdUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpProdUnique` `WithLp.toLp` `Unique.instInhabited`	—	—
`withLpUniqueProd_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `withLpUniqueProd` `WithLp.snd`	—	—
`withLpUniqueProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `WithLp` `WithLp.instProdPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpUniqueProd` `WithLp.toLp` `Unique.instInhabited`	—	—

LinearIsometry

Definitions

Name	Category	Theorems
`withLpProdCongr` 📖	CompOp	—
`withLpProdMap` 📖	CompOp	1 math math: `withLpProdMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withLpProdMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometry` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `instFunLike` `withLpProdMap` `WithLp.toLp` `WithLp.fst` `WithLp.snd`	—	—

LinearIsometryEquiv

Definitions

Name	Category	Theorems
`withLpProdAssoc` 📖	CompOp	2 math math: `withLpProdAssoc_apply`, `withLpProdAssoc_symm_apply`
`withLpProdComm` 📖	CompOp	2 math math: `withLpProdComm_symm`, `withLpProdComm_apply`
`withLpProdCongr` 📖	CompOp	2 math math: `withLpProdCongr_symm_apply`, `withLpProdCongr_apply`
`withLpProdUnique` 📖	CompOp	3 math math: `coe_withLpProdUnique`, `withLpProdUnique_symm_apply`, `withLpProdUnique_apply`
`withLpUniqueProd` 📖	CompOp	3 math math: `withLpUniqueProd_apply`, `withLpUniqueProd_symm_apply`, `coe_withLpUniqueProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_withLpProdUnique` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `withLpProdUnique` `WithLp.fst`	—	`RingHomInvPair.ids`
`coe_withLpUniqueProd` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `withLpUniqueProd` `WithLp.snd`	—	`RingHomInvPair.ids`
`withLpProdAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `EquivLike.toFunLike` `instEquivLike` `withLpProdAssoc` `WithLp.toLp` `WithLp.fst` `WithLp.snd`	—	`RingHomInvPair.ids`
`withLpProdAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpProdAssoc` `WithLp.toLp` `WithLp.fst` `WithLp.snd`	—	`RingHomInvPair.ids`
`withLpProdComm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `withLpProdComm` `WithLp.toLp` `WithLp.snd` `WithLp.fst`	—	`RingHomInvPair.ids`
`withLpProdComm_symm` 📖	mathematical	—	`symm` `WithLp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `withLpProdComm`	—	`RingHomInvPair.ids`
`withLpProdCongr_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `withLpProdCongr` `WithLp.toLp` `WithLp.fst` `WithLp.snd`	—	`RingHomInvPair.ids`
`withLpProdCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpProdCongr` `WithLp.toLp` `LinearEquiv` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `LinearEquiv.prodCongr` `toLinearEquiv` `WithLp.ofLp`	—	`RingHomInvPair.ids`
`withLpProdUnique_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `withLpProdUnique` `WithLp.fst`	—	`RingHomInvPair.ids`
`withLpProdUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpProdUnique` `WithLp.toLp` `Unique.instInhabited`	—	`RingHomInvPair.ids`
`withLpUniqueProd_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `withLpUniqueProd` `WithLp.snd`	—	`RingHomInvPair.ids`
`withLpUniqueProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `WithLp.instProdSeminormedAddCommGroup` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `withLpUniqueProd` `WithLp.toLp` `Unique.instInhabited`	—	`RingHomInvPair.ids`

WithLp

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	61 math math: `MeasureTheory.integrable_prodLp_iff`, `prod_edist_eq_card`, `norm_fst_le`, `Submodule.orthogonalDecomposition_symm_apply`, `edist_fst_le`, `prod_nndist_eq_of_L2`, `MeasureTheory.fst_integral_withLp`, `ofLp_fst`, `prod_nnnorm_eq_add`, `IsometryEquiv.withLpProdUnique_apply`, `sub_fst`, `nndist_fst_le`, `continuous_fst`, `prod_dist_eq_of_L2`, `prod_norm_eq_of_nat`, `prod_nndist_eq_of_L1`, `zero_fst`, `prod_edist_eq_of_L2`, `prod_edist_eq_sup`, `prod_norm_eq_add`, `prod_nnnorm_eq_of_L2`, `prod_nnnorm_eq_of_L1`, `prod_dist_eq_sup`, `IsometryEquiv.coe_withLpProdUnique`, `Submodule.fst_orthogonalDecomposition_apply`, `prod_nndist_eq_add`, `prod_norm_eq_of_L1`, `prod_dist_eq_add`, `toLp_fst`, `LinearIsometryEquiv.coe_withLpProdUnique`, `prod_dist_eq_of_L1`, `prod_dist_eq_card`, `nnnorm_fst_le`, `prod_norm_eq_sup`, `prod_norm_eq_card`, `prod_norm_sq_eq_of_L2`, `smul_fst`, `prod_edist_eq_of_L1`, `prod_nndist_eq_sup`, `neg_fst`, `prod_nnnorm_eq_sup`, `LinearIsometryEquiv.withLpProdCongr_apply`, `MeasureTheory.MemLp.prodLp_fst`, `IsometryEquiv.withLpProdAssoc_apply`, `MeasureTheory.memLp_prodLp_iff`, `add_fst`, `idemFst_apply`, `LinearIsometryEquiv.withLpProdUnique_apply`, `LinearIsometry.withLpProdMap_apply`, `LinearIsometryEquiv.withLpProdComm_apply`, `IsometryEquiv.withLpProdAssoc_symm_apply`, `LinearIsometryEquiv.withLpProdAssoc_apply`, `IsometryEquiv.withLpProdComm_apply`, `prod_norm_eq_of_L2`, `fstL_apply`, `enorm_fst_le`, `prod_edist_eq_add`, `MeasureTheory.Integrable.prodLp_fst`, `LinearIsometryEquiv.withLpProdAssoc_symm_apply`, `fstₗ_apply`, `dist_fst_le`
`fstL` 📖	CompOp	3 math math: `coe_fstL`, `Submodule.fstL_comp_coe_orthogonalDecomposition`, `fstL_apply`
`fstₗ` 📖	CompOp	2 math math: `coe_fstL`, `fstₗ_apply`
`homeomorphProd` 📖	CompOp	2 math math: `toEquiv_homeomorphProd`, `toHomeomorph_uniformEquivProd`
`idemFst` 📖	CompOp	7 math math: `prod_norm_eq_idemFst_of_L1`, `idemSnd_compl`, `prod_norm_eq_idemFst_sup_idemSnd`, `prod_norm_eq_add_idemFst`, `idemFst_compl`, `idemFst_add_idemSnd`, `idemFst_apply`
`idemSnd` 📖	CompOp	7 math math: `prod_norm_eq_idemFst_of_L1`, `idemSnd_compl`, `prod_norm_eq_idemFst_sup_idemSnd`, `prod_norm_eq_add_idemFst`, `idemFst_compl`, `idemSnd_apply`, `idemFst_add_idemSnd`
`instProdBornology` 📖	CompOp	—
`instProdDist` 📖	CompOp	10 math math: `prod_dist_eq_of_L2`, `dist_snd_le`, `prod_dist_eq_sup`, `dist_toLp_snd`, `prod_dist_eq_add`, `prod_dist_eq_of_L1`, `prod_dist_eq_card`, `dist_pseudoMetricSpaceToProd`, `dist_toLp_fst`, `dist_fst_le`
`instProdEDist` 📖	CompOp	11 math math: `prod_edist_eq_card`, `edist_fst_le`, `edist_toLp_snd`, `prod_edist_eq_of_L2`, `prod_edist_eq_sup`, `prod_edist_eq_of_L1`, `prod_edist_self`, `edist_toLp_fst`, `prod_edist_eq_add`, `edist_snd_le`, `prod_edist_comm`
`instProdEMetricSpace` 📖	CompOp	—
`instProdMetricSpace` 📖	CompOp	—
`instProdNorm` 📖	CompOp	18 math math: `norm_fst_le`, `prod_norm_eq_idemFst_of_L1`, `prod_norm_toLp`, `prod_norm_eq_of_nat`, `prod_norm_ofLp`, `prod_norm_eq_idemFst_sup_idemSnd`, `prod_norm_eq_add`, `prod_norm_eq_add_idemFst`, `norm_toLp_fst`, `prod_norm_eq_of_L1`, `prod_norm_eq_sup`, `prod_norm_eq_card`, `prod_norm_sq_eq_of_L2`, `instProdNormSMulClass`, `norm_seminormedAddCommGroupToProd`, `norm_snd_le`, `norm_toLp_snd`, `prod_norm_eq_of_L2`
`instProdNormedAddCommGroup` 📖	CompOp	16 math math: `MeasureTheory.fst_integral_withLp`, `NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq`, `OrthonormalBasis.prod_apply`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `contDiff_toLp`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `contDiff_ofLp`, `analyticOn_toLp`, `NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice`, `NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice`, `MeasureTheory.charFunDual_prod'`, `ProbabilityTheory.HasGaussianLaw.toLp_prodMk`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `MeasureTheory.charFunDual_eq_prod_iff'`, `MeasureTheory.snd_integral_withLp`, `analyticOn_ofLp`
`instProdNormedSpace` 📖	CompOp	10 math math: `MeasureTheory.fst_integral_withLp`, `contDiff_toLp`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `contDiff_ofLp`, `analyticOn_toLp`, `NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice`, `MeasureTheory.charFunDual_prod'`, `MeasureTheory.charFunDual_eq_prod_iff'`, `MeasureTheory.snd_integral_withLp`, `analyticOn_ofLp`
`instProdPseudoEMetricSpace` 📖	CompOp	18 math math: `IsometryEquiv.withLpUniqueProd_symm_apply`, `IsometryEquiv.withLpProdUnique_apply`, `prod_isometry_ofLp_infty`, `Isometry.withLpProdMap`, `IsometryEquiv.coe_withLpProdUnique`, `prod_antilipschitzWith_toLp`, `prod_lipschitzWith_ofLp`, `prod_lipschitzWith_toLp`, `IsometryEquiv.withLpProdCongr_apply`, `IsometryEquiv.coe_withLpUniqueProd`, `IsometryEquiv.withLpProdUnique_symm_apply`, `IsometryEquiv.withLpProdAssoc_apply`, `IsometryEquiv.withLpUniqueProd_apply`, `IsometryEquiv.withLpProdComm_symm`, `IsometryEquiv.withLpProdAssoc_symm_apply`, `IsometryEquiv.withLpProdCongr_symm_apply`, `IsometryEquiv.withLpProdComm_apply`, `prod_antilipschitzWith_ofLp`
`instProdPseudoMetricSpace` 📖	CompOp	9 math math: `prod_nndist_eq_of_L2`, `nndist_fst_le`, `prod_nndist_eq_of_L1`, `prod_nndist_eq_add`, `nndist_toLp_snd`, `prod_nndist_eq_sup`, `nndist_toLp_fst`, `instProdIsBoundedSMul`, `nndist_snd_le`
`instProdSeminormedAddCommGroup` 📖	CompOp	46 math math: `MeasureTheory.integrable_prodLp_iff`, `prod_inner_apply`, `Submodule.orthogonalDecomposition_symm_apply`, `Submodule.toLinearEquiv_orthogonalDecomposition_symm`, `LinearIsometryEquiv.withLpProdComm_symm`, `nnnorm_toLp_inr`, `prod_nnnorm_ofLp`, `Submodule.toLinearEquiv_orthogonalDecomposition`, `enorm_snd_le`, `prod_nnnorm_eq_add`, `Submodule.coe_orthogonalDecomposition_symm`, `nnnorm_seminormedAddCommGroupToProd`, `PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp`, `MeasureTheory.charFun_eq_prod_iff`, `prod_nnnorm_eq_of_L2`, `prod_nnnorm_eq_of_L1`, `Submodule.coe_orthogonalDecomposition`, `Submodule.fst_orthogonalDecomposition_apply`, `LinearIsometryEquiv.withLpProdCongr_symm_apply`, `MeasureTheory.MemLp.of_fst_of_snd_prodLp`, `ProbabilityTheory.indepFun_iff_charFun_prod`, `Submodule.sndL_comp_coe_orthogonalDecomposition`, `nnnorm_toLp_inl`, `LinearIsometryEquiv.coe_withLpProdUnique`, `nnnorm_fst_le`, `prod_nnnorm_eq_sup`, `nnnorm_snd_le`, `MeasureTheory.Integrable.of_fst_of_snd_prodLp`, `LinearIsometryEquiv.withLpProdCongr_apply`, `LinearIsometryEquiv.withLpProdUnique_symm_apply`, `MeasureTheory.memLp_prodLp_iff`, `prod_nnnorm_toLp`, `LinearIsometryEquiv.withLpProdUnique_apply`, `Submodule.fstL_comp_coe_orthogonalDecomposition`, `LinearIsometry.withLpProdMap_apply`, `Submodule.snd_orthogonalDecomposition_apply`, `LinearIsometryEquiv.withLpProdComm_apply`, `LinearIsometryEquiv.withLpProdAssoc_apply`, `Submodule.orthogonalDecomposition_apply`, `LinearIsometryEquiv.withLpUniqueProd_apply`, `MeasureTheory.charFun_prod`, `enorm_fst_le`, `LinearIsometryEquiv.withLpUniqueProd_symm_apply`, `PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp`, `LinearIsometryEquiv.withLpProdAssoc_symm_apply`, `LinearIsometryEquiv.coe_withLpUniqueProd`
`instProdTopologicalSpace` 📖	CompOp	31 math math: `MeasureTheory.integrable_prodLp_iff`, `sndL_apply`, `prodContinuousLinearEquiv_symm_apply`, `instProdT0Space`, `Submodule.coe_orthogonalDecomposition_symm`, `continuous_fst`, `borelSpace`, `NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `Submodule.coe_orthogonalDecomposition`, `prodContinuousLinearEquiv_symm_apply_ofLp`, `coe_fstL`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `MeasureTheory.MemLp.of_fst_of_snd_prodLp`, `prod_continuous_toLp`, `Submodule.sndL_comp_coe_orthogonalDecomposition`, `NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice`, `MeasureTheory.Integrable.of_fst_of_snd_prodLp`, `MeasureTheory.charFunDual_prod'`, `coe_sndL`, `MeasureTheory.memLp_prodLp_iff`, `toEquiv_homeomorphProd`, `Submodule.fstL_comp_coe_orthogonalDecomposition`, `ProbabilityTheory.HasGaussianLaw.toLp_prodMk`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `fstL_apply`, `MeasureTheory.charFunDual_eq_prod_iff'`, `prod_continuous_ofLp`, `secondCountableTopology`, `continuous_snd`, `prodContinuousLinearEquiv_apply`
`instProdUniformSpace` 📖	CompOp	6 math math: `toEquiv_uniformEquivProd`, `instProdCompleteSpace`, `prod_uniformContinuous_ofLp`, `isUniformInducing_toLp`, `toHomeomorph_uniformEquivProd`, `prod_uniformContinuous_toLp`
`normedAddCommGroupToProd` 📖	CompOp	—
`normedSpaceSeminormedAddCommGroupToProd` 📖	CompOp	—
`prodContinuousLinearEquiv` 📖	CompOp	8 math math: `prodContinuousLinearEquiv_symm_apply`, `Submodule.coe_orthogonalDecomposition_symm`, `Submodule.coe_orthogonalDecomposition`, `prodContinuousLinearEquiv_symm_apply_ofLp`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `MeasureTheory.charFunDual_prod'`, `MeasureTheory.charFunDual_eq_prod_iff'`, `prodContinuousLinearEquiv_apply`
`prodEquivₗᵢ` 📖	CompOp	—
`prodPseudoEMetricAux` 📖	CompOp	—
`prodPseudoMetricAux` 📖	CompOp	—
`pseudoMetricSpaceToProd` 📖	CompOp	2 math math: `isBoundedSMulSeminormedAddCommGroupToProd`, `dist_pseudoMetricSpaceToProd`
`seminormedAddCommGroupToProd` 📖	CompOp	3 math math: `nnnorm_seminormedAddCommGroupToProd`, `normSMulClassSeminormedAddCommGroupToProd`, `norm_seminormedAddCommGroupToProd`
`snd` 📖	CompOp	61 math math: `MeasureTheory.integrable_prodLp_iff`, `prod_edist_eq_card`, `Submodule.orthogonalDecomposition_symm_apply`, `prod_nndist_eq_of_L2`, `enorm_snd_le`, `sndL_apply`, `toLp_snd`, `smul_snd`, `prod_nnnorm_eq_add`, `neg_snd`, `prod_dist_eq_of_L2`, `prod_norm_eq_of_nat`, `prod_nndist_eq_of_L1`, `MeasureTheory.Integrable.prodLp_snd`, `prod_edist_eq_of_L2`, `prod_edist_eq_sup`, `add_snd`, `dist_snd_le`, `prod_norm_eq_add`, `prod_nnnorm_eq_of_L2`, `prod_nnnorm_eq_of_L1`, `prod_dist_eq_sup`, `prod_nndist_eq_add`, `prod_norm_eq_of_L1`, `prod_dist_eq_add`, `prod_dist_eq_of_L1`, `prod_dist_eq_card`, `IsometryEquiv.coe_withLpUniqueProd`, `prod_norm_eq_sup`, `MeasureTheory.MemLp.prodLp_snd`, `sndₗ_apply`, `prod_norm_eq_card`, `prod_norm_sq_eq_of_L2`, `prod_edist_eq_of_L1`, `prod_nndist_eq_sup`, `prod_nnnorm_eq_sup`, `idemSnd_apply`, `nnnorm_snd_le`, `LinearIsometryEquiv.withLpProdCongr_apply`, `IsometryEquiv.withLpProdAssoc_apply`, `IsometryEquiv.withLpUniqueProd_apply`, `MeasureTheory.memLp_prodLp_iff`, `sub_snd`, `zero_snd`, `norm_snd_le`, `ofLp_snd`, `LinearIsometry.withLpProdMap_apply`, `Submodule.snd_orthogonalDecomposition_apply`, `LinearIsometryEquiv.withLpProdComm_apply`, `IsometryEquiv.withLpProdAssoc_symm_apply`, `LinearIsometryEquiv.withLpProdAssoc_apply`, `IsometryEquiv.withLpProdComm_apply`, `LinearIsometryEquiv.withLpUniqueProd_apply`, `prod_norm_eq_of_L2`, `prod_edist_eq_add`, `edist_snd_le`, `nndist_snd_le`, `LinearIsometryEquiv.withLpProdAssoc_symm_apply`, `MeasureTheory.snd_integral_withLp`, `LinearIsometryEquiv.coe_withLpUniqueProd`, `continuous_snd`
`sndL` 📖	CompOp	3 math math: `sndL_apply`, `Submodule.sndL_comp_coe_orthogonalDecomposition`, `coe_sndL`
`sndₗ` 📖	CompOp	2 math math: `sndₗ_apply`, `coe_sndL`
`uniformEquivProd` 📖	CompOp	2 math math: `toEquiv_uniformEquivProd`, `toHomeomorph_uniformEquivProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_fst` 📖	mathematical	—	`fst` `WithLp` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`add_snd` 📖	mathematical	—	`snd` `WithLp` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`coe_fstL` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `instProdTopologicalSpace` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instModule` `Prod.instModule` `fstL` `fstₗ`	—	—
`coe_sndL` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `instProdTopologicalSpace` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instModule` `Prod.instModule` `sndL` `sndₗ`	—	—
`continuous_fst` 📖	mathematical	—	`Continuous` `WithLp` `instProdTopologicalSpace` `fst`	—	`Continuous.comp` `continuous_fst` `prod_continuous_ofLp`
`continuous_snd` 📖	mathematical	—	`Continuous` `WithLp` `instProdTopologicalSpace` `snd`	—	`Continuous.comp` `continuous_snd` `prod_continuous_ofLp`
`dist_fst_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `fst` `WithLp` `instProdDist`	—	`nndist_fst_le`
`dist_pseudoMetricSpaceToProd` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpaceToProd` `WithLp` `instProdDist` `toLp`	—	—
`dist_snd_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `snd` `WithLp` `instProdDist`	—	`nndist_snd_le`
`dist_toLp_fst` 📖	mathematical	—	`Dist.dist` `WithLp` `instProdDist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`nndist_toLp_fst`
`dist_toLp_snd` 📖	mathematical	—	`Dist.dist` `WithLp` `instProdDist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`nndist_toLp_snd`
`edist_fst_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `fst` `WithLp` `instProdEDist`	—	—
`edist_snd_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `snd` `WithLp` `instProdEDist`	—	—
`edist_toLp_fst` 📖	mathematical	—	`EDist.edist` `WithLp` `instProdEDist` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`edist_nndist` `nndist_toLp_fst`
`edist_toLp_snd` 📖	mathematical	—	`EDist.edist` `WithLp` `instProdEDist` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`edist_nndist` `nndist_toLp_snd`
`enorm_fst_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `fst` `WithLp` `instProdSeminormedAddCommGroup`	—	`edist_zero_right` `edist_fst_le`
`enorm_snd_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `snd` `WithLp` `instProdSeminormedAddCommGroup`	—	`edist_zero_right` `edist_snd_le`
`fstL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `instProdTopologicalSpace` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instModule` `Prod.instModule` `ContinuousLinearMap.funLike` `fstL` `fst`	—	—
`fstₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instModule` `Prod.instModule` `LinearMap.instFunLike` `fstₗ` `fst`	—	—
`idemFst_add_idemSnd` 📖	mathematical	—	`AddMonoid.End` `WithLp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoid.End.instRing` `idemFst` `idemSnd` `AddMonoid.End.instOne`	—	`AddMonoidHom.ext` `AddMonoidHom.add_apply` `idemFst_apply` `idemSnd_apply` `AddMonoid.End.coe_one` `toLp_add` `zero_add` `add_zero`
`idemFst_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoid.End` `WithLp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoid.End.instFunLike` `idemFst` `toLp` `fst` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`idemFst_compl` 📖	mathematical	—	`AddMonoid.End` `WithLp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoid.End.instRing` `AddMonoid.End.instOne` `idemFst` `idemSnd`	—	`idemFst_add_idemSnd` `add_sub_cancel_left`
`idemSnd_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoid.End` `WithLp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoid.End.instFunLike` `idemSnd` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `snd`	—	—
`idemSnd_compl` 📖	mathematical	—	`AddMonoid.End` `WithLp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoid.End.instRing` `AddMonoid.End.instOne` `idemSnd` `idemFst`	—	`idemFst_add_idemSnd` `add_sub_cancel_right`
`instProdCompleteSpace` 📖	mathematical	—	`CompleteSpace` `WithLp` `instProdUniformSpace`	—	`UniformEquiv.completeSpace_iff` `CompleteSpace.prod`
`instProdIsBoundedSMul` 📖	mathematical	—	`IsBoundedSMul` `WithLp` `SeminormedRing.toPseudoMetricSpace` `instProdPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `instSMul` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`IsBoundedSMul.of_nnnorm_smul_le` `ENNReal.dichotomy` `norm_smul_le` `Prod.instIsBoundedSMul` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ENNReal.toReal_pos_iff_ne_top` `prod_nnnorm_eq_add` `one_div` `NNReal.rpow_inv_le_iff` `NNReal.mul_rpow` `NNReal.rpow_mul` `inv_mul_cancel₀` `LT.lt.ne'` `NNReal.rpow_one` `mul_add` `Distrib.leftDistribClass` `add_le_add` `NNReal.addLeftMono` `covariant_swap_add_of_covariant_add` `NNReal.rpow_le_rpow` `nnnorm_smul_le` `LT.lt.le`
`instProdNormSMulClass` 📖	mathematical	—	`NormSMulClass` `WithLp` `SeminormedRing.toNorm` `instProdNorm` `SeminormedAddCommGroup.toNorm` `instSMul` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`NormSMulClass.of_nnnorm_smul` `ENNReal.dichotomy` `fact_one_le_top_ennreal` `nnnorm_smul` `Prod.instNormSMulClass` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ENNReal.toReal_pos_iff_ne_top` `prod_nnnorm_eq_add` `one_div` `NNReal.rpow_inv_eq_iff` `LT.lt.ne'` `NNReal.mul_rpow` `NNReal.rpow_mul` `inv_mul_cancel₀` `NNReal.rpow_one` `mul_add` `Distrib.leftDistribClass` `smul_fst` `smul_snd`
`instProdT0Space` 📖	mathematical	—	`T0Space` `WithLp` `instProdTopologicalSpace`	—	`Homeomorph.t0Space` `Prod.instT0Space`
`isBoundedSMulSeminormedAddCommGroupToProd` 📖	mathematical	—	`IsBoundedSMul` `SeminormedRing.toPseudoMetricSpace` `pseudoMetricSpaceToProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `Prod.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`dist_zero_right` `dist_smul_pair` `instProdIsBoundedSMul` `dist_pair_smul`
`isUniformInducing_toLp` 📖	mathematical	—	`IsUniformInducing` `WithLp` `instUniformSpaceProd` `PseudoEMetricSpace.toUniformSpace` `instProdUniformSpace` `toLp`	—	`AntilipschitzWith.isUniformInducing` `prod_antilipschitzWith_toLp` `LipschitzWith.uniformContinuous` `Nat.instAtLeastTwoHAddOfNat` `prod_lipschitzWith_toLp`
`neg_fst` 📖	mathematical	—	`fst` `WithLp` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`neg_snd` 📖	mathematical	—	`snd` `WithLp` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`nndist_fst_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `fst` `WithLp` `instProdPseudoMetricSpace`	—	`edist_fst_le`
`nndist_snd_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `snd` `WithLp` `instProdPseudoMetricSpace`	—	`edist_snd_le`
`nndist_toLp_fst` 📖	mathematical	—	`NNDist.nndist` `WithLp` `PseudoMetricSpace.toNNDist` `instProdPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`nndist_eq_nnnorm` `toLp_sub` `sub_zero` `nnnorm_toLp_inl`
`nndist_toLp_snd` 📖	mathematical	—	`NNDist.nndist` `WithLp` `PseudoMetricSpace.toNNDist` `instProdPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`nndist_eq_nnnorm` `toLp_sub` `sub_zero` `nnnorm_toLp_inr`
`nnnorm_fst_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `fst` `WithLp` `instProdSeminormedAddCommGroup`	—	`nndist_zero_right` `nndist_fst_le`
`nnnorm_seminormedAddCommGroupToProd` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `seminormedAddCommGroupToProd` `WithLp` `instProdSeminormedAddCommGroup` `toLp`	—	—
`nnnorm_snd_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `snd` `WithLp` `instProdSeminormedAddCommGroup`	—	`nndist_zero_right` `nndist_snd_le`
`nnnorm_toLp_inl` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`fact_one_le_top_ennreal` `prod_nnnorm_eq_sup` `nnnorm_zero` `sup_of_le_left` `NNReal.instCanonicallyOrderedAdd` `Nat.cast_zero` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `Fact.out` `prod_nnnorm_eq_add` `NNReal.zero_rpow` `add_zero` `one_div` `mul_inv_cancel₀` `NNReal.rpow_one`
`nnnorm_toLp_inr` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`fact_one_le_top_ennreal` `prod_nnnorm_eq_sup` `nnnorm_zero` `sup_of_le_right` `NNReal.instCanonicallyOrderedAdd` `Nat.cast_zero` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `Fact.out` `prod_nnnorm_eq_add` `NNReal.zero_rpow` `zero_add` `one_div` `mul_inv_cancel₀` `NNReal.rpow_one`
`normSMulClassSeminormedAddCommGroupToProd` 📖	mathematical	—	`NormSMulClass` `SeminormedRing.toNorm` `SeminormedAddCommGroup.toNorm` `seminormedAddCommGroupToProd` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_smul` `instProdNormSMulClass`
`norm_fst_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `fst` `WithLp` `instProdNorm`	—	`dist_zero_right` `dist_fst_le`
`norm_seminormedAddCommGroupToProd` 📖	mathematical	—	`Norm.norm` `SeminormedAddCommGroup.toNorm` `seminormedAddCommGroupToProd` `WithLp` `instProdNorm` `toLp`	—	—
`norm_snd_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `snd` `WithLp` `instProdNorm`	—	`dist_zero_right` `dist_snd_le`
`norm_toLp_fst` 📖	mathematical	—	`Norm.norm` `WithLp` `instProdNorm` `SeminormedAddCommGroup.toNorm` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`nnnorm_toLp_inl`
`norm_toLp_snd` 📖	mathematical	—	`Norm.norm` `WithLp` `instProdNorm` `SeminormedAddCommGroup.toNorm` `toLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`nnnorm_toLp_inr`
`ofLp_fst` 📖	mathematical	—	`ofLp` `fst`	—	—
`ofLp_snd` 📖	mathematical	—	`ofLp` `snd`	—	—
`prodContinuousLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp` `instProdTopologicalSpace` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `instModule` `Prod.instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `prodContinuousLinearEquiv` `ofLp`	—	`RingHomInvPair.ids`
`prodContinuousLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `WithLp` `instProdTopologicalSpace` `instAddCommGroup` `Prod.instAddCommGroup` `Prod.instModule` `instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `prodContinuousLinearEquiv` `toLp`	—	`RingHomInvPair.ids`
`prodContinuousLinearEquiv_symm_apply_ofLp` 📖	mathematical	—	`ofLp` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `WithLp` `instProdTopologicalSpace` `instAddCommGroup` `Prod.instAddCommGroup` `Prod.instModule` `instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `prodContinuousLinearEquiv`	—	`RingHomInvPair.ids`
`prod_antilipschitzWith_ofLp` 📖	mathematical	—	`AntilipschitzWith` `WithLp` `instProdPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `NNReal` `Real` `NNReal.instPowReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.toReal` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toOne` `instAddCommMonoidWithOneENNReal` `ofLp`	—	—
`prod_antilipschitzWith_toLp` 📖	mathematical	—	`AntilipschitzWith` `WithLp` `Prod.pseudoEMetricSpaceMax` `instProdPseudoEMetricSpace` `NNReal` `instOneNNReal` `toLp`	—	`LipschitzWith.to_rightInverse` `prod_lipschitzWith_ofLp` `ofLp_toLp`
`prod_continuous_ofLp` 📖	mathematical	—	`Continuous` `WithLp` `instProdTopologicalSpace` `instTopologicalSpaceProd` `ofLp`	—	`continuous_induced_dom`
`prod_continuous_toLp` 📖	mathematical	—	`Continuous` `WithLp` `instTopologicalSpaceProd` `instProdTopologicalSpace` `toLp`	—	`continuous_induced_rng` `continuous_id`
`prod_dist_eq_add` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ENNReal.toReal`	`Dist.dist` `WithLp` `instProdDist` `Real.instPow` `Real.instAdd` `fst` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`ENNReal.toReal_pos_iff` `LT.lt.ne'` `LT.lt.ne`
`prod_dist_eq_card` 📖	mathematical	—	`Dist.dist` `WithLp` `ENNReal` `instZeroENNReal` `instProdDist` `Real` `Real.instAdd` `fst` `Real.instZero` `Real.decidableEq` `Real.instOne` `snd`	—	—
`prod_dist_eq_of_L1` 📖	mathematical	—	`Dist.dist` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instProdDist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instAdd` `fst` `snd`	—	`fact_one_le_one_ennreal` `dist_eq_norm` `prod_norm_eq_of_L1`
`prod_dist_eq_of_L2` 📖	mathematical	—	`Dist.dist` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `instProdDist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.sqrt` `Real` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid` `fst` `snd`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `dist_eq_norm` `prod_norm_eq_of_L2`
`prod_dist_eq_sup` 📖	mathematical	—	`Dist.dist` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `instProdDist` `Real` `Real.instMax` `fst` `snd`	—	—
`prod_edist_comm` 📖	mathematical	—	`EDist.edist` `WithLp` `instProdEDist` `PseudoEMetricSpace.toEDist`	—	`ENNReal.trichotomy` `prod_edist_eq_card` `PseudoEMetricSpace.edist_comm` `prod_edist_eq_add`
`prod_edist_eq_add` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ENNReal.toReal`	`EDist.edist` `WithLp` `instProdEDist` `ENNReal` `ENNReal.instPowReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `fst` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`ENNReal.toReal_pos_iff` `LT.lt.ne'` `LT.lt.ne`
`prod_edist_eq_card` 📖	mathematical	—	`EDist.edist` `WithLp` `ENNReal` `instZeroENNReal` `instProdEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `fst` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `snd`	—	—
`prod_edist_eq_of_L1` 📖	mathematical	—	`EDist.edist` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instProdEDist` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `fst` `snd`	—	`prod_edist_eq_add` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ENNReal.rpow_one` `div_self`
`prod_edist_eq_of_L2` 📖	mathematical	—	`EDist.edist` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `instProdEDist` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `ENNReal.instPowReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `fst` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast`	—	`Nat.instAtLeastTwoHAddOfNat` `prod_edist_eq_add` `ENNReal.toReal_ofNat` `Real.instIsOrderedRing` `Real.instNontrivial` `ENNReal.rpow_ofNat` `one_div`
`prod_edist_eq_sup` 📖	mathematical	—	`EDist.edist` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `instProdEDist` `ENNReal.instMax` `fst` `snd`	—	—
`prod_edist_self` 📖	mathematical	—	`EDist.edist` `WithLp` `instProdEDist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal`	—	`ENNReal.trichotomy` `prod_edist_eq_card` `PseudoEMetricSpace.edist_self` `add_zero` `max_self` `prod_edist_eq_add` `ENNReal.zero_rpow_of_pos` `one_div` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`prod_isometry_ofLp_infty` 📖	mathematical	—	`Isometry` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `instProdPseudoEMetricSpace` `fact_one_le_top_ennreal` `Prod.pseudoEMetricSpaceMax` `ofLp`	—	`le_antisymm` `fact_one_le_top_ennreal` `one_mul` `prod_lipschitzWith_ofLp` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.div_top` `NNReal.rpow_zero` `prod_antilipschitzWith_ofLp`
`prod_lipschitzWith_ofLp` 📖	mathematical	—	`LipschitzWith` `WithLp` `instProdPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `NNReal` `instOneNNReal` `ofLp`	—	—
`prod_lipschitzWith_toLp` 📖	mathematical	—	`LipschitzWith` `WithLp` `Prod.pseudoEMetricSpaceMax` `instProdPseudoEMetricSpace` `NNReal` `Real` `NNReal.instPowReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.toReal` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toOne` `instAddCommMonoidWithOneENNReal` `toLp`	—	`AntilipschitzWith.to_rightInverse` `Nat.instAtLeastTwoHAddOfNat` `prod_antilipschitzWith_ofLp` `ofLp_toLp`
`prod_nndist_eq_add` 📖	mathematical	—	`NNDist.nndist` `WithLp` `PseudoMetricSpace.toNNDist` `instProdPseudoMetricSpace` `NNReal` `Real` `NNReal.instPowReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `fst` `ENNReal.toReal` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`NNReal.eq` `prod_dist_eq_add` `ENNReal.toReal_pos_iff_ne_top`
`prod_nndist_eq_of_L1` 📖	mathematical	—	`NNDist.nndist` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PseudoMetricSpace.toNNDist` `instProdPseudoMetricSpace` `fact_one_le_one_ennreal` `SeminormedAddCommGroup.toPseudoMetricSpace` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `fst` `snd`	—	`NNReal.eq` `fact_one_le_one_ennreal` `prod_dist_eq_of_L1`
`prod_nndist_eq_of_L2` 📖	mathematical	—	`NNDist.nndist` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `PseudoMetricSpace.toNNDist` `instProdPseudoMetricSpace` `fact_one_le_two_ennreal` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `fst` `snd`	—	`Nat.instAtLeastTwoHAddOfNat` `NNReal.eq` `fact_one_le_two_ennreal` `Real.coe_sqrt` `prod_dist_eq_of_L2`
`prod_nndist_eq_sup` 📖	mathematical	—	`NNDist.nndist` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `PseudoMetricSpace.toNNDist` `instProdPseudoMetricSpace` `fact_one_le_top_ennreal` `NNReal` `NNReal.instMax` `fst` `snd`	—	`NNReal.eq` `fact_one_le_top_ennreal` `NNReal.coe_max` `prod_dist_eq_sup`
`prod_nnnorm_eq_add` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `NNReal` `Real` `NNReal.instPowReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `fst` `ENNReal.toReal` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`NNReal.eq` `prod_norm_eq_add` `ENNReal.toReal_pos_iff_ne_top` `one_div`
`prod_nnnorm_eq_of_L1` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `fact_one_le_one_ennreal` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `fst` `snd`	—	`NNReal.eq` `fact_one_le_one_ennreal` `prod_norm_eq_of_L1`
`prod_nnnorm_eq_of_L2` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `fact_one_le_two_ennreal` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `fst` `snd`	—	`Nat.instAtLeastTwoHAddOfNat` `NNReal.eq` `fact_one_le_two_ennreal` `Real.coe_sqrt` `prod_norm_eq_of_L2`
`prod_nnnorm_eq_sup` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `fact_one_le_top_ennreal` `NNReal` `NNReal.instMax` `fst` `snd`	—	`NNReal.eq` `fact_one_le_top_ennreal`
`prod_nnnorm_ofLp` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `Prod.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ofLp` `Top.top` `ENNReal` `instTopENNReal` `WithLp` `instProdSeminormedAddCommGroup` `fact_one_le_top_ennreal`	—	`fact_one_le_top_ennreal` `prod_nnnorm_eq_sup` `Prod.nnnorm_def` `ofLp_fst` `ofLp_snd`
`prod_nnnorm_toLp` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instProdSeminormedAddCommGroup` `fact_one_le_top_ennreal` `toLp` `Prod.seminormedAddGroup`	—	`fact_one_le_top_ennreal` `prod_nnnorm_ofLp`
`prod_norm_eq_add` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ENNReal.toReal`	`Norm.norm` `WithLp` `instProdNorm` `Real.instPow` `Real.instAdd` `fst` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`ENNReal.toReal_pos_iff` `LT.lt.ne'` `LT.lt.ne`
`prod_norm_eq_add_idemFst` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ENNReal.toReal`	`Norm.norm` `WithLp` `instProdNorm` `SeminormedAddCommGroup.toNorm` `Real.instPow` `Real.instAdd` `DFunLike.coe` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoid.End.instFunLike` `idemFst` `idemSnd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`prod_norm_eq_add` `norm_toLp_fst` `norm_toLp_snd`
`prod_norm_eq_card` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `instZeroENNReal` `instProdNorm` `Real` `Real.instAdd` `fst` `Real.instZero` `Real.decidableEq` `Real.instOne` `snd`	—	—
`prod_norm_eq_idemFst_of_L1` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instProdNorm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instAdd` `DFunLike.coe` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoid.End.instFunLike` `idemFst` `idemSnd`	—	`prod_norm_eq_add_idemFst` `fact_one_le_one_ennreal` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ENNReal.toReal_one` `Real.rpow_one` `div_self`
`prod_norm_eq_idemFst_sup_idemSnd` 📖	mathematical	—	`Norm.norm` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `instProdNorm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instMax` `DFunLike.coe` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoid.End.instFunLike` `idemFst` `idemSnd`	—	`prod_norm_eq_sup` `norm_toLp_fst` `fact_one_le_top_ennreal` `norm_toLp_snd`
`prod_norm_eq_of_L1` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instProdNorm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instAdd` `fst` `snd`	—	`prod_norm_eq_add` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.rpow_one` `div_self`
`prod_norm_eq_of_L2` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `instProdNorm` `SeminormedAddCommGroup.toNorm` `Real.sqrt` `Real` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid` `fst` `snd`	—	`Nat.instAtLeastTwoHAddOfNat` `prod_norm_eq_of_nat` `fact_one_le_two_ennreal` `ENNReal.instCharZero` `Real.sqrt_eq_rpow` `Nat.cast_one`
`prod_norm_eq_of_nat` 📖	mathematical	`ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Norm.norm` `WithLp` `instProdNorm` `Real` `Real.instPow` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid` `fst` `snd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast`	—	`ENNReal.toReal_pos_iff_ne_top` `ne_of_eq_of_ne` `ENNReal.natCast_ne_top` `prod_norm_eq_add` `ENNReal.toReal_natCast` `Real.rpow_natCast` `one_div`
`prod_norm_eq_sup` 📖	mathematical	—	`Norm.norm` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `instProdNorm` `Real` `Real.instMax` `fst` `snd`	—	—
`prod_norm_ofLp` 📖	mathematical	—	`Norm.norm` `Prod.toNorm` `SeminormedAddCommGroup.toNorm` `ofLp` `Top.top` `ENNReal` `instTopENNReal` `WithLp` `instProdNorm`	—	`fact_one_le_top_ennreal` `prod_nnnorm_ofLp`
`prod_norm_sq_eq_of_L2` 📖	mathematical	—	`Real` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `instProdNorm` `SeminormedAddCommGroup.toNorm` `Real.instAdd` `fst` `snd`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `prod_nnnorm_eq_of_L2` `NNReal.sq_sqrt`
`prod_norm_toLp` 📖	mathematical	—	`Norm.norm` `WithLp` `Top.top` `ENNReal` `instTopENNReal` `instProdNorm` `SeminormedAddCommGroup.toNorm` `toLp` `Prod.toNorm`	—	`prod_norm_ofLp`
`prod_sup_edist_ne_top_aux` 📖	—	—	—	—	`ne_of_lt` `PseudoMetricSpace.edist_dist`
`prod_uniformContinuous_ofLp` 📖	mathematical	—	`UniformContinuous` `WithLp` `instProdUniformSpace` `instUniformSpaceProd` `ofLp`	—	`uniformContinuous_comap`
`prod_uniformContinuous_toLp` 📖	mathematical	—	`UniformContinuous` `WithLp` `instUniformSpaceProd` `instProdUniformSpace` `toLp`	—	`uniformContinuous_comap'` `uniformContinuous_id`
`secondCountableTopology` 📖	mathematical	—	`SecondCountableTopology` `WithLp` `instProdTopologicalSpace`	—	`Homeomorph.secondCountableTopology` `TopologicalSpace.instSecondCountableTopologyProd`
`smul_fst` 📖	mathematical	—	`fst` `WithLp` `instSMul` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	—
`smul_snd` 📖	mathematical	—	`snd` `WithLp` `instSMul` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	—
`sndL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `instProdTopologicalSpace` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instModule` `Prod.instModule` `ContinuousLinearMap.funLike` `sndL` `snd`	—	—
`sndₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `instModule` `Prod.instModule` `LinearMap.instFunLike` `sndₗ` `snd`	—	—
`sub_fst` 📖	mathematical	—	`fst` `WithLp` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`sub_snd` 📖	mathematical	—	`snd` `WithLp` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`toEquiv_homeomorphProd` 📖	mathematical	—	`Homeomorph.toEquiv` `WithLp` `instProdTopologicalSpace` `instTopologicalSpaceProd` `homeomorphProd` `equiv`	—	—
`toEquiv_uniformEquivProd` 📖	mathematical	—	`UniformEquiv.toEquiv` `WithLp` `instProdUniformSpace` `instUniformSpaceProd` `uniformEquivProd` `equiv`	—	—
`toHomeomorph_uniformEquivProd` 📖	mathematical	—	`UniformEquiv.toHomeomorph` `WithLp` `instProdUniformSpace` `instUniformSpaceProd` `uniformEquivProd` `homeomorphProd` `UniformSpace.toTopologicalSpace`	—	—
`toLp_fst` 📖	mathematical	—	`fst` `toLp`	—	—
`toLp_snd` 📖	mathematical	—	`snd` `toLp`	—	—
`zero_fst` 📖	mathematical	—	`fst` `WithLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup`	—	—
`zero_snd` 📖	mathematical	—	`snd` `WithLp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup`	—	—

---

← Back to Index