Documentation

Mathlib.Topology.Instances.TrivSqZeroExt

Topology on TrivSqZeroExt R M #

The type TrivSqZeroExt R M inherits the topology from R × M.

Note that this is not the topology induced by the seminorm on the dual numbers suggested by this Math.SE answer, which instead induces the topology pulled back through the projection map TrivSqZeroExt.fst : tsze R M → R. Obviously, that topology is not Hausdorff and using it would result in exp converging to more than one value.

Main results #

source
instance TrivSqZeroExt.instTopologicalSpace {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] :
TopologicalSpace (TrivSqZeroExt R M)
Equations
source
instance TrivSqZeroExt.instT2SpaceTrivSqZeroExtInstTopologicalSpace {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [T2Space R] [T2Space M] :
T2Space (TrivSqZeroExt R M)
Equations
source
theorem TrivSqZeroExt.nhds_def {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] (x : TrivSqZeroExt R M) :
nhds x = Filter.prod (nhds (TrivSqZeroExt.fst x)) (nhds (TrivSqZeroExt.snd x))
source
theorem TrivSqZeroExt.nhds_inl {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero M] (x : R) :
nhds (TrivSqZeroExt.inl x) = Filter.prod (nhds x) (nhds 0)
source
theorem TrivSqZeroExt.nhds_inr {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero R] (m : M) :
nhds (TrivSqZeroExt.inr m) = Filter.prod (nhds 0) (nhds m)
source
theorem TrivSqZeroExt.continuous_fst {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] :
Continuous TrivSqZeroExt.fst
source
theorem TrivSqZeroExt.continuous_snd {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] :
Continuous TrivSqZeroExt.snd
source
theorem TrivSqZeroExt.continuous_inl {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero M] :
Continuous TrivSqZeroExt.inl
source
theorem TrivSqZeroExt.continuous_inr {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero R] :
Continuous TrivSqZeroExt.inr
source
theorem TrivSqZeroExt.embedding_inl {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero M] :
Embedding TrivSqZeroExt.inl
source
theorem TrivSqZeroExt.embedding_inr {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero R] :
Embedding TrivSqZeroExt.inr
source
@[simp]
theorem TrivSqZeroExt.fstCLM_toFun (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TrivSqZeroExt R M) :
(TrivSqZeroExt.fstCLM R M) x = TrivSqZeroExt.fst x
source
@[simp]
theorem TrivSqZeroExt.fstCLM_apply (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TrivSqZeroExt R M) :
(TrivSqZeroExt.fstCLM R M) x = TrivSqZeroExt.fst x
source
def TrivSqZeroExt.fstCLM (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] :
TrivSqZeroExt R M →L[R] R

TrivSqZeroExt.fst as a continuous linear map.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TrivSqZeroExt.sndCLM_apply (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TrivSqZeroExt R M) :
    (TrivSqZeroExt.sndCLM R M) x = TrivSqZeroExt.snd x
    source
    @[simp]
    theorem TrivSqZeroExt.sndCLM_toFun (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TrivSqZeroExt R M) :
    (TrivSqZeroExt.sndCLM R M) x = TrivSqZeroExt.snd x
    source
    def TrivSqZeroExt.sndCLM (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] :
    TrivSqZeroExt R M →L[R] M

    TrivSqZeroExt.snd as a continuous linear map.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TrivSqZeroExt.inlCLM_apply (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) :
      (TrivSqZeroExt.inlCLM R M) r = TrivSqZeroExt.inl r
      source
      @[simp]
      theorem TrivSqZeroExt.inlCLM_toFun (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) :
      (TrivSqZeroExt.inlCLM R M) r = TrivSqZeroExt.inl r
      source
      def TrivSqZeroExt.inlCLM (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] :
      R →L[R] TrivSqZeroExt R M

      TrivSqZeroExt.inl as a continuous linear map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TrivSqZeroExt.inrCLM_apply (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) :
        (TrivSqZeroExt.inrCLM R M) m = TrivSqZeroExt.inr m
        source
        @[simp]
        theorem TrivSqZeroExt.inrCLM_toFun (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) :
        (TrivSqZeroExt.inrCLM R M) m = TrivSqZeroExt.inr m
        source
        def TrivSqZeroExt.inrCLM (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] :
        M →L[R] TrivSqZeroExt R M

        TrivSqZeroExt.inr as a continuous linear map.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance TrivSqZeroExt.instContinuousAddTrivSqZeroExtInstTopologicalSpaceAdd {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Add R] [Add M] [ContinuousAdd R] [ContinuousAdd M] :
          ContinuousAdd (TrivSqZeroExt R M)
          Equations
          source
          instance TrivSqZeroExt.instContinuousMulTrivSqZeroExtInstTopologicalSpaceMul {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] [ContinuousMul R] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [ContinuousAdd M] :
          ContinuousMul (TrivSqZeroExt R M)
          Equations
          source
          instance TrivSqZeroExt.instContinuousNegTrivSqZeroExtInstTopologicalSpaceNeg {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Neg R] [Neg M] [ContinuousNeg R] [ContinuousNeg M] :
          ContinuousNeg (TrivSqZeroExt R M)
          Equations
          source
          theorem TrivSqZeroExt.topologicalSemiring {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [TopologicalSemiring R] [ContinuousAdd M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] :
          TopologicalSemiring (TrivSqZeroExt R M)

          This is not an instance due to complaints by the fails_quickly linter. At any rate, we only really care about the TopologicalRing instance below.

          source
          instance TrivSqZeroExt.instTopologicalRingTrivSqZeroExtInstTopologicalSpaceToNonUnitalNonAssocRingNonAssocRing {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] :
          TopologicalRing (TrivSqZeroExt R M)
          Equations
          source
          instance TrivSqZeroExt.instContinuousConstSMulTrivSqZeroExtInstTopologicalSpaceSmul {S : Type u_2} {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [SMul S R] [SMul S M] [ContinuousConstSMul S R] [ContinuousConstSMul S M] :
          ContinuousConstSMul S (TrivSqZeroExt R M)
          Equations
          source
          instance TrivSqZeroExt.instContinuousSMulTrivSqZeroExtSmulInstTopologicalSpace {S : Type u_2} {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace S] [SMul S R] [SMul S M] [ContinuousSMul S R] [ContinuousSMul S M] :
          ContinuousSMul S (TrivSqZeroExt R M)
          Equations
          source
          theorem TrivSqZeroExt.hasSum_inl {α : Type u_1} {R : Type u_3} (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [AddCommMonoid R] [AddCommMonoid M] {f : α → R} {a : R} (h : HasSum f a) :
          HasSum (fun (x : α) => TrivSqZeroExt.inl (f x)) (TrivSqZeroExt.inl a)
          source
          theorem TrivSqZeroExt.hasSum_inr {α : Type u_1} {R : Type u_3} (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [AddCommMonoid R] [AddCommMonoid M] {f : α → M} {a : M} (h : HasSum f a) :
          HasSum (fun (x : α) => TrivSqZeroExt.inr (f x)) (TrivSqZeroExt.inr a)
          source
          theorem TrivSqZeroExt.hasSum_fst {α : Type u_1} {R : Type u_3} (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [AddCommMonoid R] [AddCommMonoid M] {f : α → TrivSqZeroExt R M} {a : TrivSqZeroExt R M} (h : HasSum f a) :
          HasSum (fun (x : α) => TrivSqZeroExt.fst (f x)) (TrivSqZeroExt.fst a)
          source
          theorem TrivSqZeroExt.hasSum_snd {α : Type u_1} {R : Type u_3} (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [AddCommMonoid R] [AddCommMonoid M] {f : α → TrivSqZeroExt R M} {a : TrivSqZeroExt R M} (h : HasSum f a) :
          HasSum (fun (x : α) => TrivSqZeroExt.snd (f x)) (TrivSqZeroExt.snd a)
          source
          instance TrivSqZeroExt.instUniformSpace {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] :
          UniformSpace (TrivSqZeroExt R M)
          Equations
          • One or more equations did not get rendered due to their size.
          source
          instance TrivSqZeroExt.instCompleteSpaceTrivSqZeroExtInstUniformSpace {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [CompleteSpace R] [CompleteSpace M] :
          CompleteSpace (TrivSqZeroExt R M)
          Equations
          source
          instance TrivSqZeroExt.instUniformAddGroupTrivSqZeroExtInstUniformSpaceAddGroup {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [AddGroup R] [AddGroup M] [UniformAddGroup R] [UniformAddGroup M] :
          UniformAddGroup (TrivSqZeroExt R M)
          Equations
          source
          theorem TrivSqZeroExt.uniformity_def {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] :
          uniformity (TrivSqZeroExt R M) = Filter.comap (fun (p : TrivSqZeroExt R M × TrivSqZeroExt R M) => (TrivSqZeroExt.fst p.1, TrivSqZeroExt.fst p.2)) (uniformity R) ⊓ Filter.comap (fun (p : TrivSqZeroExt R M × TrivSqZeroExt R M) => (TrivSqZeroExt.snd p.1, TrivSqZeroExt.snd p.2)) (uniformity M)
          source
          theorem TrivSqZeroExt.uniformContinuous_fst {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] :
          UniformContinuous TrivSqZeroExt.fst
          source
          theorem TrivSqZeroExt.uniformContinuous_snd {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] :
          UniformContinuous TrivSqZeroExt.snd
          source
          theorem TrivSqZeroExt.uniformContinuous_inl {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [Zero M] :
          UniformContinuous TrivSqZeroExt.inl
          source
          theorem TrivSqZeroExt.uniformContinuous_inr {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [Zero R] :
          UniformContinuous TrivSqZeroExt.inr