mathlib3 documentation

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]

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.

theorem triv_sq_zero_ext.has_sum_inl {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α R} {a : R} (h : has_sum f a) :
theorem triv_sq_zero_ext.has_sum_inr {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α M} {a : M} (h : has_sum f a) :
theorem triv_sq_zero_ext.has_sum_fst {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α triv_sq_zero_ext R M} {a : triv_sq_zero_ext R M} (h : has_sum f 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) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α triv_sq_zero_ext R M} {a : triv_sq_zero_ext R M} (h : has_sum f a) :
has_sum (λ (x : α), (f x).snd) a.snd