Mathlib.Topology.Instances.TrivSqZeroExt

TrivSqZeroExt.instTopologicalSpace instance

: TopologicalSpace (tsze R M)

Full source

instance instTopologicalSpace : TopologicalSpace (tsze R M) :=
  TopologicalSpace.inducedTopologicalSpace.induced fst ‹_› ⊓ TopologicalSpace.induced snd ‹_›

Topological Space Structure on Trivial Square-Zero Extensions

Informal description

The trivial square-zero extension $\text{tsze}\, R\, M$ is equipped with the product topology inherited from $R \times M$.

TrivSqZeroExt.instT2Space instance

[T2Space R] [T2Space M] : T2Space (tsze R M)

Full source

instance [T2Space R] [T2Space M] : T2Space (tsze R M) :=
  Prod.t2Space

Hausdorff Property of Trivial Square-Zero Extensions

Informal description

For any topological spaces $R$ and $M$ that are Hausdorff, the trivial square-zero extension $\text{tsze}\, R\, M$ is also a Hausdorff space.

TrivSqZeroExt.nhds_def theorem

(x : tsze R M) : 𝓝 x = 𝓝 x.fst ×ˢ 𝓝 x.snd

Full source

theorem nhds_def (x : tsze R M) : 𝓝 x = 𝓝 x.fst ×ˢ 𝓝 x.snd := nhds_prod_eq

Neighborhood Filter Decomposition in Trivial Square-Zero Extension

Informal description

For any element $x$ in the trivial square-zero extension $\text{tsze}\, R\, M$, the neighborhood filter $\mathcal{N}(x)$ is equal to the product filter $\mathcal{N}(x.fst) \times \mathcal{N}(x.snd)$, where $x.fst$ and $x.snd$ are the projections of $x$ to $R$ and $M$ respectively.

TrivSqZeroExt.nhds_inl theorem

[Zero M] (x : R) : 𝓝 (inl x : tsze R M) = 𝓝 x ×ˢ 𝓝 0

Full source

theorem nhds_inl [Zero M] (x : R) : 𝓝 (inl x : tsze R M) = 𝓝 x ×ˢ 𝓝 0 :=
  nhds_def _

Neighborhood Filter of Left Inclusion in Trivial Square-Zero Extension

Informal description

For any topological space $R$ and any topological module $M$ over $R$ with zero element $0 \in M$, the neighborhood filter of the element $\mathrm{inl}\, x$ in the trivial square-zero extension $\mathrm{tsze}\, R\, M$ is equal to the product filter $\mathcal{N}(x) \times \mathcal{N}(0)$, where $\mathcal{N}(x)$ is the neighborhood filter of $x$ in $R$ and $\mathcal{N}(0)$ is the neighborhood filter of $0$ in $M$.

TrivSqZeroExt.nhds_inr theorem

[Zero R] (m : M) : 𝓝 (inr m : tsze R M) = 𝓝 0 ×ˢ 𝓝 m

Full source

theorem nhds_inr [Zero R] (m : M) : 𝓝 (inr m : tsze R M) = 𝓝 0 ×ˢ 𝓝 m :=
  nhds_def _

Neighborhood Filter of Right Injection in Trivial Square-Zero Extension

Informal description

For any element $m$ in the module $M$ over a ring $R$ with zero element $0$, the neighborhood filter $\mathcal{N}(\mathrm{inr}\, m)$ of the element $\mathrm{inr}\, m$ in the trivial square-zero extension $\text{tsze}\, R\, M$ is equal to the product filter $\mathcal{N}(0) \times \mathcal{N}(m)$, where $\mathcal{N}(0)$ is the neighborhood filter of $0$ in $R$ and $\mathcal{N}(m)$ is the neighborhood filter of $m$ in $M$.

TrivSqZeroExt.continuous_fst theorem

: Continuous (fst : tsze R M → R)

Full source

nonrec theorem continuous_fst : Continuous (fst : tsze R M → R) :=
  continuous_fst

Continuity of First Projection in Trivial Square-Zero Extensions

Informal description

The projection map $\mathrm{fst} : R \times M \to R$ is continuous, where $R \times M$ is equipped with the product topology.

TrivSqZeroExt.continuous_snd theorem

: Continuous (snd : tsze R M → M)

Full source

nonrec theorem continuous_snd : Continuous (snd : tsze R M → M) :=
  continuous_snd

Continuity of the Second Projection in Trivial Square-Zero Extensions

Informal description

The projection map $\text{snd} : \text{tsze}\, R\, M \to M$ is continuous, where $\text{tsze}\, R\, M$ is equipped with the product topology inherited from $R \times M$.

TrivSqZeroExt.continuous_inl theorem

[Zero M] : Continuous (inl : R → tsze R M)

Full source

theorem continuous_inl [Zero M] : Continuous (inl : R → tsze R M) :=
  continuous_id.prodMk continuous_const

Continuity of the Left Injection in Trivial Square-Zero Extensions

Informal description

Let $R$ and $M$ be topological spaces with $M$ containing a zero element. The canonical injection map $\text{inl} : R \to \text{tsze}\, R\, M$ is continuous, where $\text{tsze}\, R\, M$ is equipped with the product topology inherited from $R \times M$.

TrivSqZeroExt.continuous_inr theorem

[Zero R] : Continuous (inr : M → tsze R M)

Full source

theorem continuous_inr [Zero R] : Continuous (inr : M → tsze R M) :=
  continuous_const.prodMk continuous_id

Continuity of the Right Injection in Trivial Square-Zero Extensions

Informal description

When $R$ has a zero element, the canonical injection map $\text{inr} : M \to \text{tsze}\, R\, M$ is continuous, where $\text{tsze}\, R\, M$ is equipped with the product topology inherited from $R \times M$.

TrivSqZeroExt.IsEmbedding.inl theorem

[Zero M] : IsEmbedding (inl : R → tsze R M)

Full source

theorem IsEmbedding.inl [Zero M] : IsEmbedding (inl : R → tsze R M) :=
  .of_comp continuous_inl continuous_fst .id

Embedding Property of the Left Injection in Trivial Square-Zero Extensions

Informal description

Let $R$ and $M$ be topological spaces with $M$ containing a zero element. The canonical injection map $\mathrm{inl} : R \to \mathrm{tsze}\, R\, M$ is an embedding, where $\mathrm{tsze}\, R\, M$ is equipped with the product topology inherited from $R \times M$.

TrivSqZeroExt.IsEmbedding.inr theorem

[Zero R] : IsEmbedding (inr : M → tsze R M)

Full source

theorem IsEmbedding.inr [Zero R] : IsEmbedding (inr : M → tsze R M) :=
  .of_comp continuous_inr continuous_snd .id

Embedding Property of the Right Injection in Trivial Square-Zero Extensions

Informal description

When $R$ has a zero element, the canonical injection map $\text{inr} : M \to \text{tsze}\, R\, M$ is an embedding, where $\text{tsze}\, R\, M$ is equipped with the product topology inherited from $R \times M$.

TrivSqZeroExt.fstCLM definition

[CommSemiring R] [AddCommMonoid M] [Module R M] : tsze R M →L[R] R

Full source

/-- `TrivSqZeroExt.fst` as a continuous linear map. -/
@[simps]
def fstCLM [CommSemiring R] [AddCommMonoid M] [Module R M] : tszetsze R M →L[R] R :=
  { ContinuousLinearMap.fst R R M with toFun := fst }

Continuous linear projection from trivial square-zero extension to base ring

Informal description

The continuous linear map that projects the first component of a trivial square-zero extension $\text{tsze}\, R\, M$ to $R$, where $R$ is a commutative semiring and $M$ is an $R$-module.

TrivSqZeroExt.sndCLM definition

[CommSemiring R] [AddCommMonoid M] [Module R M] : tsze R M →L[R] M

Full source

/-- `TrivSqZeroExt.snd` as a continuous linear map. -/
@[simps]
def sndCLM [CommSemiring R] [AddCommMonoid M] [Module R M] : tszetsze R M →L[R] M :=
  { ContinuousLinearMap.snd R R M with
    toFun := snd
    cont := continuous_snd }

Continuous linear projection from trivial square-zero extension to module

Informal description

The continuous linear map that projects the second component of a trivial square-zero extension $\text{tsze}\, R\, M$ to $M$, where $R$ is a commutative semiring and $M$ is an $R$-module.

TrivSqZeroExt.inlCLM definition

[CommSemiring R] [AddCommMonoid M] [Module R M] : R →L[R] tsze R M

Full source

/-- `TrivSqZeroExt.inl` as a continuous linear map. -/
@[simps]
def inlCLM [CommSemiring R] [AddCommMonoid M] [Module R M] : R →L[R] tsze R M :=
  { ContinuousLinearMap.inl R R M with toFun := inl }

Continuous linear embedding of $R$ into trivial square-zero extension

Informal description

The continuous linear map that embeds the commutative semiring $R$ into the trivial square-zero extension $\text{tsze}\, R\, M$ by sending $r \in R$ to $(r, 0) \in R \times M$.

TrivSqZeroExt.inrCLM definition

[CommSemiring R] [AddCommMonoid M] [Module R M] : M →L[R] tsze R M

Full source

/-- `TrivSqZeroExt.inr` as a continuous linear map. -/
@[simps]
def inrCLM [CommSemiring R] [AddCommMonoid M] [Module R M] : M →L[R] tsze R M :=
  { ContinuousLinearMap.inr R R M with toFun := inr }

Continuous linear embedding of $M$ into trivial square-zero extension

Informal description

The continuous linear map that embeds the module $M$ into the trivial square-zero extension $\text{tsze}\, R\, M$ by sending $m \in M$ to $(0, m) \in R \times M$.

TrivSqZeroExt.instContinuousAdd instance

[Add R] [Add M] [ContinuousAdd R] [ContinuousAdd M] : ContinuousAdd (tsze R M)

Full source

instance [Add R] [Add M] [ContinuousAdd R] [ContinuousAdd M] : ContinuousAdd (tsze R M) :=
  Prod.continuousAdd

Continuity of Addition on Trivial Square-Zero Extensions

Informal description

For any types $R$ and $M$ with addition operations, if addition is continuous on both $R$ and $M$, then addition is also continuous on the trivial square-zero extension $\text{tsze}\, R\, M$ equipped with the product topology.

TrivSqZeroExt.instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd instance

 [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] [ContinuousMul R] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M]
  [ContinuousAdd M] : ContinuousMul (tsze R M)

Full source

instance [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] [ContinuousMul R] [ContinuousSMul R M]
    [ContinuousSMul Rᵐᵒᵖ M] [ContinuousAdd M] : ContinuousMul (tsze R M) :=
  ⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prodMk <|
      ((continuous_fst.comp continuous_fst).smul (continuous_snd.comp continuous_snd)).add
        ((MulOpposite.continuous_op.comp <| continuous_fst.comp <| continuous_snd).smul
          (continuous_snd.comp continuous_fst))⟩

Continuity of Multiplication in Trivial Square-Zero Extensions

Informal description

For any types $R$ and $M$ with multiplication on $R$, addition on $M$, and scalar multiplication actions of $R$ and its opposite ring $R^{\text{op}}$ on $M$, if multiplication is continuous on $R$, scalar multiplication is continuous for both $R$ and $R^{\text{op}}$ acting on $M$, and addition is continuous on $M$, then multiplication is continuous on the trivial square-zero extension $\text{tsze}\, R\, M$ equipped with the product topology.

TrivSqZeroExt.instContinuousNeg instance

[Neg R] [Neg M] [ContinuousNeg R] [ContinuousNeg M] : ContinuousNeg (tsze R M)

Full source

instance [Neg R] [Neg M] [ContinuousNeg R] [ContinuousNeg M] : ContinuousNeg (tsze R M) :=
  Prod.continuousNeg

Continuity of Negation on Trivial Square-Zero Extensions

Informal description

For any types $R$ and $M$ with negation operations, if negation is continuous on both $R$ and $M$, then negation is also continuous on the trivial square-zero extension $\text{tsze}\, R\, M$ equipped with the product topology.

TrivSqZeroExt.topologicalSemiring theorem

 [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsTopologicalSemiring R] [ContinuousAdd M]
  [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] : IsTopologicalSemiring (tsze R M)

Full source

/-- This is not an instance due to complaints by the `fails_quickly` linter. At any rate, we only
really care about the `IsTopologicalRing` instance below. -/
theorem topologicalSemiring [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
    [IsTopologicalSemiring R] [ContinuousAdd M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] :
    IsTopologicalSemiring (tsze R M) := { }

Trivial Square-Zero Extension as a Topological Semiring

Informal description

Let $R$ be a semiring and $M$ an additive commutative monoid, where $M$ is both a module over $R$ and its opposite ring $R^{\text{op}}$. If $R$ is a topological semiring, addition is continuous on $M$, and the scalar multiplications $R \times M \to M$ and $R^{\text{op}} \times M \to M$ are both continuous, then the trivial square-zero extension $\text{tsze}\, R\, M$ equipped with the product topology is also a topological semiring.

TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite instance

 [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsTopologicalRing R] [IsTopologicalAddGroup M]
  [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] : IsTopologicalRing (tsze R M)

Full source

instance [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsTopologicalRing R]
    [IsTopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] :
    IsTopologicalRing (tsze R M) where

Topological Ring Structure on Trivial Square-Zero Extensions

Informal description

For any ring $R$ and $R$-module $M$ with compatible actions of $R$ and its opposite ring $R^{\text{op}}$ on $M$, if $R$ is a topological ring, $M$ is a topological additive group, and the scalar multiplications of $R$ and $R^{\text{op}}$ on $M$ are continuous, then the trivial square-zero extension $\text{tsze}\, R\, M$ is a topological ring.

TrivSqZeroExt.instContinuousConstSMul instance

[SMul S R] [SMul S M] [ContinuousConstSMul S R] [ContinuousConstSMul S M] : ContinuousConstSMul S (tsze R M)

Full source

instance [SMul S R] [SMul S M] [ContinuousConstSMul S R] [ContinuousConstSMul S M] :
    ContinuousConstSMul S (tsze R M) :=
  Prod.continuousConstSMul

Continuous Scalar Multiplication on Trivial Square-Zero Extensions

Informal description

For any type $S$ with scalar multiplication actions on $R$ and $M$, if the scalar multiplication is continuous in the second variable on both $R$ and $M$, then the trivial square-zero extension $\text{tsze}\, R\, M$ also has continuous scalar multiplication in the second variable.

TrivSqZeroExt.instContinuousSMul instance

[TopologicalSpace S] [SMul S R] [SMul S M] [ContinuousSMul S R] [ContinuousSMul S M] : ContinuousSMul S (tsze R M)

Full source

instance [TopologicalSpace S] [SMul S R] [SMul S M] [ContinuousSMul S R] [ContinuousSMul S M] :
    ContinuousSMul S (tsze R M) :=
  Prod.continuousSMul

Continuous Scalar Multiplication on Trivial Square-Zero Extensions

Informal description

For any topological space $S$ with scalar multiplication actions on $R$ and $M$, if the scalar multiplication is continuous on both $R$ and $M$, then the scalar multiplication on the trivial square-zero extension $\text{tsze}\, R\, M$ is also continuous.

TrivSqZeroExt.hasSum_inl theorem

 [AddCommMonoid R] [AddCommMonoid M] {f : α → R} {a : R} (h : HasSum f a) :
  HasSum (fun x ↦ inl (f x)) (inl a : tsze R M)

Full source

theorem hasSum_inl [AddCommMonoid R] [AddCommMonoid M] {f : α → R} {a : R} (h : HasSum f a) :
    HasSum (fun x ↦ inl (f x)) (inl a : tsze R M) :=
  h.map (⟨⟨inl, inl_zero _⟩, inl_add _⟩ : R →+ tsze R M) continuous_inl

Sum Preservation of Left Injection in Trivial Square-Zero Extension

Informal description

Let $R$ and $M$ be additive commutative monoids, and let $f : α → R$ be a function with sum $a ∈ R$. Then the function $x ↦ \text{inl}(f(x))$ has sum $\text{inl}(a)$ in the trivial square-zero extension $\text{tsze}\, R\, M$.

TrivSqZeroExt.hasSum_inr theorem

 [AddCommMonoid R] [AddCommMonoid M] {f : α → M} {a : M} (h : HasSum f a) :
  HasSum (fun x ↦ inr (f x)) (inr a : tsze R M)

Full source

theorem hasSum_inr [AddCommMonoid R] [AddCommMonoid M] {f : α → M} {a : M} (h : HasSum f a) :
    HasSum (fun x ↦ inr (f x)) (inr a : tsze R M) :=
  h.map (⟨⟨inr, inr_zero _⟩, inr_add _⟩ : M →+ tsze R M) continuous_inr

Sum Preservation by Right Injection in Trivial Square-Zero Extensions

Informal description

Let $R$ and $M$ be additively commutative monoids, and let $f : \alpha \to M$ be a function with sum $a \in M$. Then the function $\text{inr} \circ f : \alpha \to \text{tsze}\, R\, M$ has sum $\text{inr}(a) \in \text{tsze}\, R\, M$, where $\text{tsze}\, R\, M$ is the trivial square-zero extension of $R$ by $M$ equipped with the product topology.

TrivSqZeroExt.hasSum_fst theorem

 [AddCommMonoid R] [AddCommMonoid M] {f : α → tsze R M} {a : tsze R M} (h : HasSum f a) :
  HasSum (fun x ↦ fst (f x)) (fst a)

Full source

theorem hasSum_fst [AddCommMonoid R] [AddCommMonoid M] {f : α → tsze R M} {a : tsze R M}
    (h : HasSum f a) : HasSum (fun x ↦ fst (f x)) (fst a) :=
  h.map (⟨⟨fst, fst_zero⟩, fst_add⟩ : tszetsze R M →+ R) continuous_fst

Sum Convergence of First Projection in Trivial Square-Zero Extensions

Informal description

Let $R$ and $M$ be additively commutative monoids, and let $f : \alpha \to \text{tsze}\, R\, M$ be a function with a sum converging to $a \in \text{tsze}\, R\, M$. Then the sum of the first projections $\text{fst} \circ f$ converges to $\text{fst}(a)$ in $R$.

TrivSqZeroExt.hasSum_snd theorem

 [AddCommMonoid R] [AddCommMonoid M] {f : α → tsze R M} {a : tsze R M} (h : HasSum f a) :
  HasSum (fun x ↦ snd (f x)) (snd a)

Full source

theorem hasSum_snd [AddCommMonoid R] [AddCommMonoid M] {f : α → tsze R M} {a : tsze R M}
    (h : HasSum f a) : HasSum (fun x ↦ snd (f x)) (snd a) :=
  h.map (⟨⟨snd, snd_zero⟩, snd_add⟩ : tszetsze R M →+ M) continuous_snd

Sum Convergence of Second Projection in Trivial Square-Zero Extensions

Informal description

Let $R$ and $M$ be additively commutative monoids, and let $f : \alpha \to \text{tsze}\, R\, M$ be a function with sum $a \in \text{tsze}\, R\, M$. Then the sum of the second projections $\text{snd} \circ f$ converges to $\text{snd}(a)$ in $M$.

TrivSqZeroExt.instUniformSpace instance

: UniformSpace (tsze R M)

Full source

instance instUniformSpace : UniformSpace (tsze R M) where
  toTopologicalSpace := instTopologicalSpace
  __ := instUniformSpaceProd

Uniform Space Structure on Trivial Square-Zero Extensions

Informal description

The trivial square-zero extension $\text{tsze}\, R\, M$ is equipped with a uniform space structure inherited from the product uniform space structure on $R \times M$.

TrivSqZeroExt.instCompleteSpace instance

[CompleteSpace R] [CompleteSpace M] : CompleteSpace (tsze R M)

Full source

instance [CompleteSpace R] [CompleteSpace M] : CompleteSpace (tsze R M) :=
  inferInstanceAs <| CompleteSpace (R × M)

Completeness of Trivial Square-Zero Extensions

Informal description

For any complete spaces $R$ and $M$, the trivial square-zero extension $\text{tsze}\, R\, M$ is also a complete space.

TrivSqZeroExt.instIsUniformAddGroup instance

[AddGroup R] [AddGroup M] [IsUniformAddGroup R] [IsUniformAddGroup M] : IsUniformAddGroup (tsze R M)

Full source

instance [AddGroup R] [AddGroup M] [IsUniformAddGroup R] [IsUniformAddGroup M] :
    IsUniformAddGroup (tsze R M) :=
  inferInstanceAs <| IsUniformAddGroup (R × M)

Uniform Additive Group Structure on Trivial Square-Zero Extensions

Informal description

For any additive groups $R$ and $M$ equipped with uniform additive group structures, the trivial square-zero extension $\text{tsze}\, R\, M$ inherits a uniform additive group structure from the product uniform space structure on $R \times M$.

TrivSqZeroExt.uniformity_def theorem

: 𝓤 (tsze R M) = ((𝓤 R).comap fun p => (p.1.fst, p.2.fst)) ⊓ ((𝓤 M).comap fun p => (p.1.snd, p.2.snd))

Full source

theorem uniformity_def :
    𝓤 (tsze R M) =
      ((𝓤 R).comap fun p => (p.1.fst, p.2.fst)) ⊓ ((𝓤 M).comap fun p => (p.1.snd, p.2.snd)) :=
  rfl

Uniformity of Trivial Square-Zero Extension as Product of Component Uniformities

Informal description

The uniformity on the trivial square-zero extension $\text{tsze}\, R\, M$ is equal to the infimum of the pullbacks of the uniformities on $R$ and $M$ via the projection maps $\text{fst} : \text{tsze}\, R\, M \to R$ and $\text{snd} : \text{tsze}\, R\, M \to M$ respectively. In other words, the uniformity is given by: \[ \mathcal{U}(\text{tsze}\, R\, M) = \left(\mathcal{U}(R) \text{ via } \text{fst}\right) \sqcap \left(\mathcal{U}(M) \text{ via } \text{snd}\right) \] where $\mathcal{U}(-)$ denotes the uniformity on a space.

TrivSqZeroExt.uniformContinuous_fst theorem

: UniformContinuous (fst : tsze R M → R)

Full source

nonrec theorem uniformContinuous_fst : UniformContinuous (fst : tsze R M → R) :=
  uniformContinuous_fst

Uniform Continuity of First Projection on Trivial Square-Zero Extensions

Informal description

The projection map $\text{fst} : \text{tsze}\, R\, M \to R$ from the trivial square-zero extension to its first component is uniformly continuous, where $\text{tsze}\, R\, M$ is equipped with the uniform space structure inherited from $R \times M$.

TrivSqZeroExt.uniformContinuous_snd theorem

: UniformContinuous (snd : tsze R M → M)

Full source

nonrec theorem uniformContinuous_snd : UniformContinuous (snd : tsze R M → M) :=
  uniformContinuous_snd

Uniform Continuity of Second Projection on Trivial Square-Zero Extensions

Informal description

The second projection map $\operatorname{snd} : \text{tsze}\, R\, M \to M$ is uniformly continuous, where $\text{tsze}\, R\, M$ is equipped with the uniform space structure inherited from $R \times M$.

TrivSqZeroExt.uniformContinuous_inl theorem

[Zero M] : UniformContinuous (inl : R → tsze R M)

Full source

theorem uniformContinuous_inl [Zero M] : UniformContinuous (inl : R → tsze R M) :=
  uniformContinuous_id.prodMk uniformContinuous_const

Uniform Continuity of the Left Inclusion in Trivial Square-Zero Extensions

Informal description

Let $R$ and $M$ be types with $M$ having a zero element. The canonical inclusion map $\text{inl}: R \to \text{tsze}\, R\, M$ is uniformly continuous, where $\text{tsze}\, R\, M$ is equipped with the uniform space structure inherited from $R \times M$.

TrivSqZeroExt.uniformContinuous_inr theorem

[Zero R] : UniformContinuous (inr : M → tsze R M)

Full source

theorem uniformContinuous_inr [Zero R] : UniformContinuous (inr : M → tsze R M) :=
  uniformContinuous_const.prodMk uniformContinuous_id

Uniform continuity of the right inclusion map into trivial square-zero extensions

Informal description

When $R$ has a zero element, the inclusion map $\text{inr} : M \to \text{tsze}\, R\, M$ is uniformly continuous, where $\text{tsze}\, R\, M$ is equipped with the uniform structure inherited from $R \times M$.

Main results