# mathlib3documentation

topology.instances.triv_sq_zero_ext

# Topology on triv_sq_zero_ext R M#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The type triv_sq_zero_ext 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 triv_sq_zero_ext.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 #

@[protected, instance]
def triv_sq_zero_ext.topological_space {R : Type u_3} {M : Type u_4}  :
Equations
@[protected, instance]
def triv_sq_zero_ext.t2_space {R : Type u_3} {M : Type u_4} [t2_space R] [t2_space M] :
theorem triv_sq_zero_ext.nhds_def {R : Type u_3} {M : Type u_4} (x : M) :
nhds x = (nhds x.fst).prod (nhds x.snd)
theorem triv_sq_zero_ext.nhds_inl {R : Type u_3} {M : Type u_4} [has_zero M] (x : R) :
= (nhds x).prod (nhds 0)
theorem triv_sq_zero_ext.nhds_inr {R : Type u_3} {M : Type u_4} [has_zero R] (m : M) :
= (nhds 0).prod (nhds m)
theorem triv_sq_zero_ext.continuous_fst {R : Type u_3} {M : Type u_4}  :
theorem triv_sq_zero_ext.continuous_snd {R : Type u_3} {M : Type u_4}  :
theorem triv_sq_zero_ext.continuous_inl {R : Type u_3} {M : Type u_4} [has_zero M] :
theorem triv_sq_zero_ext.continuous_inr {R : Type u_3} {M : Type u_4} [has_zero R] :
theorem triv_sq_zero_ext.embedding_inl {R : Type u_3} {M : Type u_4} [has_zero M] :
theorem triv_sq_zero_ext.embedding_inr {R : Type u_3} {M : Type u_4} [has_zero R] :
@[simp]
theorem triv_sq_zero_ext.fst_clm_coe_apply (R : Type u_3) (M : Type u_4) [ M] (x : M) :
x = x.fst
def triv_sq_zero_ext.fst_clm (R : Type u_3) (M : Type u_4) [ M] :
→L[R] R

triv_sq_zero_ext.fst as a continuous linear map.

Equations
@[simp]
theorem triv_sq_zero_ext.fst_clm_apply (R : Type u_3) (M : Type u_4) [ M] (x : M) :
x = x.fst
@[simp]
theorem triv_sq_zero_ext.snd_clm_coe_apply (R : Type u_3) (M : Type u_4) [ M] (x : M) :
x = x.snd
@[simp]
theorem triv_sq_zero_ext.snd_clm_apply (R : Type u_3) (M : Type u_4) [ M] (x : M) :
x = x.snd
def triv_sq_zero_ext.snd_clm (R : Type u_3) (M : Type u_4) [ M] :
→L[R] M

triv_sq_zero_ext.snd as a continuous linear map.

Equations
@[simp]
theorem triv_sq_zero_ext.inl_clm_coe_apply (R : Type u_3) (M : Type u_4) [ M] (r : R) :
def triv_sq_zero_ext.inl_clm (R : Type u_3) (M : Type u_4) [ M] :
R →L[R]

triv_sq_zero_ext.inl as a continuous linear map.

Equations
@[simp]
theorem triv_sq_zero_ext.inl_clm_apply (R : Type u_3) (M : Type u_4) [ M] (r : R) :
def triv_sq_zero_ext.inr_clm (R : Type u_3) (M : Type u_4) [ M] :
M →L[R]

triv_sq_zero_ext.inr as a continuous linear map.

Equations
@[simp]
theorem triv_sq_zero_ext.inr_clm_coe_apply (R : Type u_3) (M : Type u_4) [ M] (m : M) :
@[simp]
theorem triv_sq_zero_ext.inr_clm_apply (R : Type u_3) (M : Type u_4) [ M] (m : M) :
@[protected, instance]
@[protected, instance]
def triv_sq_zero_ext.has_continuous_mul {R : Type u_3} {M : Type u_4} [has_mul R] [has_add M] [ M] [ M] [ M]  :
@[protected, instance]
def triv_sq_zero_ext.has_continuous_neg {R : Type u_3} {M : Type u_4} [has_neg R] [has_neg M]  :
theorem triv_sq_zero_ext.topological_semiring {R : Type u_3} {M : Type u_4} [semiring R] [ M] [ M] [ M]  :

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

@[protected, instance]
def triv_sq_zero_ext.topological_ring {R : Type u_3} {M : Type u_4} [ring R] [ M] [ M] [ M]  :
@[protected, instance]
def triv_sq_zero_ext.has_continuous_const_smul {S : Type u_2} {R : Type u_3} {M : Type u_4} [ R] [ M]  :
@[protected, instance]
def triv_sq_zero_ext.has_continuous_smul {S : Type u_2} {R : Type u_3} {M : Type u_4} [ R] [ M] [ R] [ M] :
theorem triv_sq_zero_ext.has_sum_inl {α : Type u_1} {R : Type u_3} (M : Type u_4) {f : α R} {a : R} (h : a) :
has_sum (λ (x : α), triv_sq_zero_ext.inl (f x))
theorem triv_sq_zero_ext.has_sum_inr {α : Type u_1} {R : Type u_3} (M : Type u_4) {f : α M} {a : M} (h : a) :
has_sum (λ (x : α), triv_sq_zero_ext.inr (f x))
theorem triv_sq_zero_ext.has_sum_fst {α : Type u_1} {R : Type u_3} (M : Type u_4) {f : α } {a : M} (h : a) :
has_sum (λ (x : α), (f x).fst) a.fst
theorem triv_sq_zero_ext.has_sum_snd {α : Type u_1} {R : Type u_3} (M : Type u_4) {f : α } {a : M} (h : a) :
has_sum (λ (x : α), (f x).snd) a.snd