TrivSqZeroExt

📁 Source: Mathlib/Topology/Instances/TrivSqZeroExt.lean

Statistics

Metric	Count
Definitions `TrivSqZeroExt`, `fstCLM`, `inlCLM`, `inrCLM`, `instTopologicalSpace`, `instUniformSpace`, `sndCLM`	7
Theorems `inl`, `inr`, `continuous_fst`, `continuous_inl`, `continuous_inr`, `continuous_snd`, `fstCLM_apply`, `hasSum_fst`, `hasSum_inl`, `hasSum_inr`, `hasSum_snd`, `inlCLM_apply`, `inrCLM_apply`, `instCompleteSpace`, `instContinuousAdd`, `instContinuousConstSMul`, `instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd`, `instContinuousNeg`, `instContinuousSMul`, `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`, `instIsUniformAddGroup`, `instT2Space`, `nhds_def`, `nhds_inl`, `nhds_inr`, `sndCLM_apply`, `topologicalSemiring`, `uniformContinuous_fst`, `uniformContinuous_inl`, `uniformContinuous_inr`, `uniformContinuous_snd`, `uniformity_def`	32
Total	39

TrivSqZeroExt

Definitions

Name	Category	Theorems
`fstCLM` 📖	CompOp	1 math math: `fstCLM_apply`
`inlCLM` 📖	CompOp	1 math math: `inlCLM_apply`
`inrCLM` 📖	CompOp	1 math math: `inrCLM_apply`
`instTopologicalSpace` 📖	CompOp	37 math math: `fstCLM_apply`, `exp_inr`, `IsEmbedding.inr`, `instContinuousNeg`, `nhds_def`, `hasSum_inr`, `continuous_snd`, `fst_exp`, `hasSum_snd_expSeries_of_smul_comm`, `fst_expSeries`, `eq_smul_exp_of_ne_zero`, `instT2Space`, `snd_exp`, `sndCLM_apply`, `instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd`, `hasSum_inl`, `inrCLM_apply`, `DualNumber.exp_eps`, `exp_def`, `nhds_inl`, `continuous_inl`, `hasSum_expSeries_of_smul_comm`, `inlCLM_apply`, `topologicalSemiring`, `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`, `continuous_inr`, `instContinuousSMul`, `IsEmbedding.inl`, `instContinuousAdd`, `exp_inl`, `DualNumber.exp_smul_eps`, `continuous_fst`, `nhds_inr`, `exp_def_of_smul_comm`, `snd_expSeries_of_smul_comm`, `eq_smul_exp_of_invertible`, `instContinuousConstSMul`
`instUniformSpace` 📖	CompOp	7 math math: `instCompleteSpace`, `uniformContinuous_fst`, `uniformContinuous_snd`, `uniformContinuous_inr`, `instIsUniformAddGroup`, `uniformContinuous_inl`, `uniformity_def`
`sndCLM` 📖	CompOp	1 math math: `sndCLM_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_fst` 📖	mathematical	—	`Continuous` `TrivSqZeroExt` `instTopologicalSpace` `fst`	—	`continuous_fst`
`continuous_inl` 📖	mathematical	—	`Continuous` `TrivSqZeroExt` `instTopologicalSpace` `inl`	—	`Continuous.prodMk` `continuous_id` `continuous_const`
`continuous_inr` 📖	mathematical	—	`Continuous` `TrivSqZeroExt` `instTopologicalSpace` `inr`	—	`Continuous.prodMk` `continuous_const` `continuous_id`
`continuous_snd` 📖	mathematical	—	`Continuous` `TrivSqZeroExt` `instTopologicalSpace` `snd`	—	`continuous_snd`
`fstCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TrivSqZeroExt` `instTopologicalSpace` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `ContinuousLinearMap.funLike` `fstCLM` `fst`	—	—
`hasSum_fst` 📖	mathematical	`HasSum` `TrivSqZeroExt` `addCommMonoid` `instTopologicalSpace` `SummationFilter.unconditional`	`fst`	—	`HasSum.map` `AddMonoidHom.instAddMonoidHomClass` `fst_zero` `fst_add` `continuous_fst`
`hasSum_inl` 📖	mathematical	`HasSum` `SummationFilter.unconditional`	`TrivSqZeroExt` `addCommMonoid` `instTopologicalSpace` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`HasSum.map` `AddMonoidHom.instAddMonoidHomClass` `inl_zero` `inl_add` `continuous_inl`
`hasSum_inr` 📖	mathematical	`HasSum` `SummationFilter.unconditional`	`TrivSqZeroExt` `addCommMonoid` `instTopologicalSpace` `inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`HasSum.map` `AddMonoidHom.instAddMonoidHomClass` `inr_zero` `inr_add` `continuous_inr`
`hasSum_snd` 📖	mathematical	`HasSum` `TrivSqZeroExt` `addCommMonoid` `instTopologicalSpace` `SummationFilter.unconditional`	`snd`	—	`HasSum.map` `AddMonoidHom.instAddMonoidHomClass` `snd_zero` `snd_add` `continuous_snd`
`inlCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TrivSqZeroExt` `instTopologicalSpace` `addCommMonoid` `Semiring.toModule` `module` `ContinuousLinearMap.funLike` `inlCLM` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`inrCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TrivSqZeroExt` `instTopologicalSpace` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `ContinuousLinearMap.funLike` `inrCLM` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `TrivSqZeroExt` `instUniformSpace`	—	`CompleteSpace.prod`
`instContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `TrivSqZeroExt` `instTopologicalSpace` `add`	—	`Prod.continuousAdd`
`instContinuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `TrivSqZeroExt` `instTopologicalSpace` `smul`	—	`Prod.continuousConstSMul`
`instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd` 📖	mathematical	—	`ContinuousMul` `TrivSqZeroExt` `instTopologicalSpace` `mul`	—	`Continuous.prodMk` `Continuous.mul` `Continuous.comp` `continuous_fst` `continuous_snd` `Continuous.add` `Continuous.smul` `MulOpposite.continuous_op`
`instContinuousNeg` 📖	mathematical	—	`ContinuousNeg` `TrivSqZeroExt` `instTopologicalSpace` `neg`	—	`Prod.continuousNeg`
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `TrivSqZeroExt` `smul` `instTopologicalSpace`	—	`Prod.continuousSMul`
`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` 📖	mathematical	—	`IsTopologicalRing` `TrivSqZeroExt` `instTopologicalSpace` `NonAssocRing.toNonUnitalNonAssocRing` `nonAssocRing`	—	`instContinuousAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalAddGroup.toContinuousAdd` `instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd` `IsTopologicalSemiring.toContinuousMul` `instContinuousNeg` `IsTopologicalRing.toContinuousNeg` `IsTopologicalAddGroup.toContinuousNeg`
`instIsUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `TrivSqZeroExt` `instUniformSpace` `addGroup`	—	`Prod.instIsUniformAddGroup`
`instT2Space` 📖	mathematical	—	`T2Space` `TrivSqZeroExt` `instTopologicalSpace`	—	`Prod.t2Space`
`nhds_def` 📖	mathematical	—	`nhds` `TrivSqZeroExt` `instTopologicalSpace` `SProd.sprod` `Filter` `Filter.instSProd` `fst` `snd`	—	`nhds_prod_eq`
`nhds_inl` 📖	mathematical	—	`nhds` `TrivSqZeroExt` `instTopologicalSpace` `inl` `SProd.sprod` `Filter` `Filter.instSProd`	—	`nhds_def`
`nhds_inr` 📖	mathematical	—	`nhds` `TrivSqZeroExt` `instTopologicalSpace` `inr` `SProd.sprod` `Filter` `Filter.instSProd`	—	`nhds_def`
`sndCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TrivSqZeroExt` `instTopologicalSpace` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `ContinuousLinearMap.funLike` `sndCLM` `snd`	—	—
`topologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `TrivSqZeroExt` `instTopologicalSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `nonAssocSemiring`	—	`instContinuousAdd` `IsTopologicalSemiring.toContinuousAdd` `instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd` `IsTopologicalSemiring.toContinuousMul`
`uniformContinuous_fst` 📖	mathematical	—	`UniformContinuous` `TrivSqZeroExt` `instUniformSpace` `fst`	—	`uniformContinuous_fst`
`uniformContinuous_inl` 📖	mathematical	—	`UniformContinuous` `TrivSqZeroExt` `instUniformSpace` `inl`	—	`UniformContinuous.prodMk` `uniformContinuous_id` `uniformContinuous_const`
`uniformContinuous_inr` 📖	mathematical	—	`UniformContinuous` `TrivSqZeroExt` `instUniformSpace` `inr`	—	`UniformContinuous.prodMk` `uniformContinuous_const` `uniformContinuous_id`
`uniformContinuous_snd` 📖	mathematical	—	`UniformContinuous` `TrivSqZeroExt` `instUniformSpace` `snd`	—	`uniformContinuous_snd`
`uniformity_def` 📖	mathematical	—	`uniformity` `TrivSqZeroExt` `instUniformSpace` `Filter` `Filter.instInf` `Filter.comap` `fst` `snd`	—	—

TrivSqZeroExt.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl` 📖	mathematical	—	`Topology.IsEmbedding` `TrivSqZeroExt` `TrivSqZeroExt.instTopologicalSpace` `TrivSqZeroExt.inl`	—	`Topology.IsEmbedding.of_comp` `TrivSqZeroExt.continuous_inl` `TrivSqZeroExt.continuous_fst` `Topology.IsEmbedding.id`
`inr` 📖	mathematical	—	`Topology.IsEmbedding` `TrivSqZeroExt` `TrivSqZeroExt.instTopologicalSpace` `TrivSqZeroExt.inr`	—	`Topology.IsEmbedding.of_comp` `TrivSqZeroExt.continuous_inr` `TrivSqZeroExt.continuous_snd` `Topology.IsEmbedding.id`

(root)

Definitions

Name	Category	Theorems
`TrivSqZeroExt` 📖	CompOp	178 math math: `TrivSqZeroExt.fstCLM_apply`, `TrivSqZeroExt.exp_inr`, `TrivSqZeroExt.IsEmbedding.inr`, `TrivSqZeroExt.snd_pow`, `TrivSqZeroExt.instCompleteSpace`, `TrivSqZeroExt.lift_inlAlgHom_inrHom`, `TrivSqZeroExt.instContinuousNeg`, `TrivSqZeroExt.snd_pow_eq_sum`, `TrivSqZeroExt.nhds_def`, `TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst`, `TensorAlgebra.toTrivSqZeroExt_ι`, `TrivSqZeroExt.hasSum_inr`, `TrivSqZeroExt.fst_intCast`, `TrivSqZeroExt.inv_inl`, `TrivSqZeroExt.inl_fst_add_inr_snd_eq`, `TrivSqZeroExt.inv_one`, `TrivSqZeroExt.isScalarTower`, `ExteriorAlgebra.toTrivSqZeroExt_comp_map`, `TrivSqZeroExt.snd_list_prod`, `TrivSqZeroExt.fstHom_comp_map`, `TrivSqZeroExt.instNormOneClass`, `TrivSqZeroExt.continuous_snd`, `TrivSqZeroExt.snd_add`, `TrivSqZeroExt.fst_exp`, `TrivSqZeroExt.map_inr`, `TrivSqZeroExt.uniformContinuous_fst`, `TrivSqZeroExt.fst_smul`, `TrivSqZeroExt.snd_surjective`, `TrivSqZeroExt.lift_comp_inrHom`, `TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm`, `TrivSqZeroExt.fst_invOf`, `TrivSqZeroExt.fst_expSeries`, `TrivSqZeroExt.algHom_ext'_iff`, `TrivSqZeroExt.fst_comp_inr`, `TrivSqZeroExt.map_comp_inlAlgHom`, `TrivSqZeroExt.eq_smul_exp_of_ne_zero`, `TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf`, `TrivSqZeroExt.uniformContinuous_snd`, `TrivSqZeroExt.inl_mul_inr`, `TrivSqZeroExt.fst_list_prod`, `TrivSqZeroExt.algebraMap_eq_inl'`, `TrivSqZeroExt.instT2Space`, `TrivSqZeroExt.isNilpotent_inr`, `TrivSqZeroExt.norm_def`, `DualNumber.lift_inlAlgHom_eps`, `TrivSqZeroExt.inl_injective`, `TrivSqZeroExt.mul_left_eq_one`, `TrivSqZeroExt.snd_exp`, `TrivSqZeroExt.map_comp_inrHom`, `TrivSqZeroExt.inl_add`, `TrivSqZeroExt.sndCLM_apply`, `TrivSqZeroExt.fst_add`, `TrivSqZeroExt.uniformContinuous_inr`, `TrivSqZeroExt.fst_sum`, `TrivSqZeroExt.inl_smul`, `TrivSqZeroExt.inr_mul_inr`, `TrivSqZeroExt.fst_one`, `TrivSqZeroExt.instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd`, `TrivSqZeroExt.lift_apply_inr`, `TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf`, `TrivSqZeroExt.inlHom_apply`, `TrivSqZeroExt.hasSum_inl`, `TrivSqZeroExt.isNilpotent_inl_iff`, `TrivSqZeroExt.mul_inv_cancel`, `TrivSqZeroExt.inv_mul_cancel`, `TrivSqZeroExt.invOf_eq_inv`, `TrivSqZeroExt.inl_neg`, `TrivSqZeroExt.snd_inv`, `TrivSqZeroExt.liftEquiv_apply`, `TrivSqZeroExt.inl_mul`, `TrivSqZeroExt.inlAlgHom_apply`, `TrivSqZeroExt.instNontrivial_of_left`, `TrivSqZeroExt.inrCLM_apply`, `TrivSqZeroExt.snd_smul`, `TrivSqZeroExt.smulCommClass`, `TrivSqZeroExt.inv_inv`, `TrivSqZeroExt.inrHom_apply`, `TrivSqZeroExt.inr_neg`, `TrivSqZeroExt.instIsUniformAddGroup`, `TrivSqZeroExt.inl_natCast`, `TrivSqZeroExt.exp_def`, `TrivSqZeroExt.inr_mul_inl`, `ExteriorAlgebra.toTrivSqZeroExt_ι`, `TrivSqZeroExt.snd_invOf`, `TrivSqZeroExt.inl_mul_inl`, `TrivSqZeroExt.nhds_inl`, `TrivSqZeroExt.continuous_inl`, `TrivSqZeroExt.hasSum_expSeries_of_smul_comm`, `TrivSqZeroExt.snd_pow_of_smul_comm`, `TrivSqZeroExt.snd_sum`, `TrivSqZeroExt.isCentralScalar`, `TrivSqZeroExt.liftEquivOfComm_apply`, `TrivSqZeroExt.isUnit_inv_iff`, `TrivSqZeroExt.fst_neg`, `TrivSqZeroExt.inlCLM_apply`, `TrivSqZeroExt.inv_neg`, `TrivSqZeroExt.fst_inv`, `TrivSqZeroExt.inr_sub`, `TrivSqZeroExt.sndHom_comp_map`, `TrivSqZeroExt.map_comp_map`, `TrivSqZeroExt.norm_inl`, `TrivSqZeroExt.inr_smul`, `TrivSqZeroExt.instL1IsBoundedSMul`, `TrivSqZeroExt.snd_mul`, `TrivSqZeroExt.topologicalSemiring`, `TrivSqZeroExt.snd_pow_of_smul_comm'`, `TrivSqZeroExt.fst_pow`, `TrivSqZeroExt.lift_def`, `TrivSqZeroExt.algebraMap_eq_inl`, `DualNumber.range_inlAlgHom_sup_adjoin_eps`, `TrivSqZeroExt.nnnorm_def`, `TrivSqZeroExt.inr_injective`, `TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`, `TrivSqZeroExt.continuous_inr`, `TrivSqZeroExt.snd_comp_inr`, `TrivSqZeroExt.isUnit_inr_iff`, `TrivSqZeroExt.nnnorm_inl`, `TrivSqZeroExt.instContinuousSMul`, `TrivSqZeroExt.isUnit_or_isNilpotent_of_isMaximal_isNilpotent`, `TrivSqZeroExt.snd_map`, `TrivSqZeroExt.IsEmbedding.inl`, `TrivSqZeroExt.snd_natCast`, `TrivSqZeroExt.fst_comp_inl`, `TrivSqZeroExt.instContinuousAdd`, `TrivSqZeroExt.fst_map`, `TrivSqZeroExt.lift_comp_inlHom`, `TrivSqZeroExt.inr_add`, `TrivSqZeroExt.liftEquivOfComm_symm_apply_coe`, `TrivSqZeroExt.fst_natCast`, `TrivSqZeroExt.algebraMap_eq_inlHom`, `TrivSqZeroExt.lift_apply_inl`, `TrivSqZeroExt.exp_inl`, `TrivSqZeroExt.inl_sum`, `TrivSqZeroExt.sndHom_apply`, `TrivSqZeroExt.snd_one`, `TrivSqZeroExt.inl_zero`, `TrivSqZeroExt.map_inl`, `TrivSqZeroExt.continuous_fst`, `TrivSqZeroExt.nnnorm_inr`, `TrivSqZeroExt.nhds_inr`, `TrivSqZeroExt.mul_right_eq_one`, `TrivSqZeroExt.fst_mul`, `TrivSqZeroExt.inr_zero`, `TrivSqZeroExt.exp_def_of_smul_comm`, `TrivSqZeroExt.snd_neg`, `TrivSqZeroExt.uniformContinuous_inl`, `TrivSqZeroExt.inl_mul_eq_smul`, `TrivSqZeroExt.instNontrivial_of_right`, `TrivSqZeroExt.inv_zero`, `TrivSqZeroExt.isUnit_inl_iff`, `TrivSqZeroExt.instIsScalarTower`, `TrivSqZeroExt.isUnit_iff_isUnit_fst`, `TrivSqZeroExt.inl_intCast`, `TrivSqZeroExt.snd_sub`, `TrivSqZeroExt.fstHom_apply`, `TrivSqZeroExt.liftEquiv_symm_apply_coe`, `TrivSqZeroExt.isUnit_or_isNilpotent`, `TrivSqZeroExt.fst_surjective`, `TrivSqZeroExt.mul_inv_rev`, `TrivSqZeroExt.inl_pow`, `TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr`, `TrivSqZeroExt.snd_zero`, `TrivSqZeroExt.inr_sum`, `TrivSqZeroExt.mul_inl_eq_op_smul`, `TrivSqZeroExt.fst_sub`, `TrivSqZeroExt.inl_sub`, `TrivSqZeroExt.snd_comp_inl`, `TrivSqZeroExt.uniformity_def`, `TrivSqZeroExt.snd_expSeries_of_smul_comm`, `TrivSqZeroExt.inv_inr`, `TrivSqZeroExt.eq_smul_exp_of_invertible`, `TrivSqZeroExt.map_id`, `TrivSqZeroExt.range_liftAux`, `TrivSqZeroExt.norm_inr`, `TrivSqZeroExt.fst_zero`, `TrivSqZeroExt.inl_one`, `TrivSqZeroExt.snd_intCast`, `TrivSqZeroExt.instContinuousConstSMul`

---

← Back to Index