mathlib documentation

topology.algebra.module

Theory of topological modules and continuous linear maps. #

We use the class has_continuous_smul for topological (semi) modules and topological vector spaces.

In this file we define continuous linear maps, as linear maps between topological modules which are continuous. The set of continuous linear maps between the topological R-modules M and M₂ is denoted by M →L[R] M₂.

Continuous linear equivalences are denoted by M ≃L[R] M₂.

theorem submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [has_continuous_smul R M] [has_continuous_add M] [(𝓝[{x : R | is_unit x}] 0).ne_bot] (s : submodule R M) (hs : (interior s).nonempty) :
s =

If M is a topological module over R and 0 is a limit of invertible elements of R, then is the only submodule of M with a nonempty interior. This is the case, e.g., if R is a nondiscrete normed field.

theorem submodule.closure_smul_self_subset {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] (s : submodule R M) :
(λ (p : R × M), p.fst p.snd) '' set.univ.prod (closure s) closure s
theorem submodule.closure_smul_self_eq {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] (s : submodule R M) :
(λ (p : R × M), p.fst p.snd) '' set.univ.prod (closure s) = closure s

The (topological-space) closure of a submodule of a topological R-module M is itself a submodule.

Equations
structure continuous_linear_map (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max u_2 u_3)

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

@[nolint]
structure continuous_linear_equiv (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max u_2 u_3)

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Properties that hold for non-necessarily commutative semirings. #

@[instance]
def continuous_linear_map.linear_map.has_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
has_coe (M →L[R] M₂) (M →ₗ[R] M₂)

Coerce continuous linear maps to linear maps.

Equations
@[simp]
theorem continuous_linear_map.to_linear_map_eq_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
@[instance]
def continuous_linear_map.to_fun {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :

Coerce continuous linear maps to functions.

Equations
@[simp]
theorem continuous_linear_map.coe_mk {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (h : continuous f.to_fun . "continuity'") :
{to_linear_map := f, cont := h} = f
@[simp]
theorem continuous_linear_map.coe_mk' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (h : continuous f.to_fun . "continuity'") :
theorem continuous_linear_map.continuous {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
theorem continuous_linear_map.coe_injective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.coe_inj {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M →L[R] M₂} :
f = g f = g
theorem continuous_linear_map.coe_fn_injective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[ext]
theorem continuous_linear_map.ext {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M →L[R] M₂} (h : ∀ (x : M), f x = g x) :
f = g
theorem continuous_linear_map.ext_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M →L[R] M₂} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem continuous_linear_map.map_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
f 0 = 0
@[simp]
theorem continuous_linear_map.map_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (x y : M) :
f (x + y) = f x + f y
@[simp]
theorem continuous_linear_map.map_smul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (c : R) (x : M) :
f (c x) = c f x
@[simp]
theorem continuous_linear_map.map_smul_of_tower {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_4} [semiring S] [has_scalar R M] [module S M] [has_scalar R M₂] [module S M₂] [linear_map.compatible_smul M M₂ R S] (f : M →L[S] M₂) (c : R) (x : M) :
f (c x) = c f x
theorem continuous_linear_map.map_sum {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) {ι : Type u_4} (s : finset ι) (g : ι → M) :
f (∑ (i : ι) in s, g i) = ∑ (i : ι) in s, f (g i)
@[simp]
theorem continuous_linear_map.coe_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
@[ext]
theorem continuous_linear_map.ext_ring {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] [topological_space R] {f g : R →L[R] M} (h : f 1 = g 1) :
f = g
theorem continuous_linear_map.ext_ring_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] [topological_space R] {f g : R →L[R] M} :
f = g f 1 = g 1
theorem continuous_linear_map.eq_on_closure_span {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [t2_space M₂] {s : set M} {f g : M →L[R] M₂} (h : set.eq_on f g s) :

If two continuous linear maps are equal on a set s, then they are equal on the closure of the submodule.span of this set.

theorem continuous_linear_map.ext_on {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [t2_space M₂] {s : set M} (hs : dense (submodule.span R s)) {f g : M →L[R] M₂} (h : set.eq_on f g s) :
f = g

If the submodule generated by a set s is dense in the ambient module, then two continuous linear maps equal on s are equal.

Under a continuous linear map, the image of the topological_closure of a submodule is contained in the topological_closure of its image.

Under a dense continuous linear map, a submodule whose topological_closure is is sent to another such submodule. That is, the image of a dense set under a map with dense range is dense.

@[instance]
def continuous_linear_map.has_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
has_zero (M →L[R] M₂)

The continuous map that is constantly zero.

Equations
@[instance]
def continuous_linear_map.inhabited {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
inhabited (M →L[R] M₂)
Equations
@[simp]
theorem continuous_linear_map.default_def {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
default (M →L[R] M₂) = 0
@[simp]
theorem continuous_linear_map.zero_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (x : M) :
0 x = 0
@[simp]
theorem continuous_linear_map.coe_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
0 = 0
theorem continuous_linear_map.coe_zero' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
0 = 0
def continuous_linear_map.id (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] [module R M] :
M →L[R] M

the identity map as a continuous linear map.

Equations
@[instance]
def continuous_linear_map.has_one {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] :
Equations
theorem continuous_linear_map.one_def {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] :
theorem continuous_linear_map.id_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (x : M) :
@[simp]
@[simp]
theorem continuous_linear_map.coe_id' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] :
@[simp]
theorem continuous_linear_map.coe_eq_id {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {f : M →L[R] M} :
@[simp]
theorem continuous_linear_map.one_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (x : M) :
1 x = x
@[instance]
def continuous_linear_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [has_continuous_add M₂] :
has_add (M →L[R] M₂)
Equations
theorem continuous_linear_map.continuous_nsmul {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [has_continuous_add M₂] (n : ) :
continuous (λ (x : M₂), n x)
theorem continuous_linear_map.continuous.nsmul {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [has_continuous_add M₂] {α : Type u_1} [topological_space α] {n : } {f : α → M₂} (hf : continuous f) :
continuous (λ (x : α), n f x)
@[simp]
theorem continuous_linear_map.add_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) (x : M) [has_continuous_add M₂] :
(f + g) x = f x + g x
@[simp]
theorem continuous_linear_map.coe_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) [has_continuous_add M₂] :
(f + g) = f + g
theorem continuous_linear_map.coe_add' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) [has_continuous_add M₂] :
(f + g) = f + g
@[instance]
def continuous_linear_map.add_comm_monoid {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [has_continuous_add M₂] :
Equations
@[simp]
theorem continuous_linear_map.coe_sum {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [has_continuous_add M₂] {ι : Type u_4} (t : finset ι) (f : ι → (M →L[R] M₂)) :
∑ (d : ι) in t, f d = ∑ (d : ι) in t, (f d)
@[simp]
theorem continuous_linear_map.coe_sum' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [has_continuous_add M₂] {ι : Type u_4} (t : finset ι) (f : ι → (M →L[R] M₂)) :
∑ (d : ι) in t, f d = ∑ (d : ι) in t, (f d)
theorem continuous_linear_map.sum_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] [has_continuous_add M₂] {ι : Type u_4} (t : finset ι) (f : ι → (M →L[R] M₂)) (b : M) :
(∑ (d : ι) in t, f d) b = ∑ (d : ι) in t, (f d) b
def continuous_linear_map.comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (g : M₂ →L[R] M₃) (f : M →L[R] M₂) :
M →L[R] M₃

Composition of bounded linear maps.

Equations
@[simp]
theorem continuous_linear_map.coe_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) (h : M₂ →L[R] M₃) :
(h.comp f) = h.comp f
@[simp]
theorem continuous_linear_map.coe_comp' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) (h : M₂ →L[R] M₃) :
(h.comp f) = h f
@[simp]
theorem continuous_linear_map.comp_id {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
@[simp]
theorem continuous_linear_map.id_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
@[simp]
theorem continuous_linear_map.comp_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) :
f.comp 0 = 0
@[simp]
theorem continuous_linear_map.zero_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) :
0.comp f = 0
@[simp]
theorem continuous_linear_map.comp_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₂] [has_continuous_add M₃] (g : M₂ →L[R] M₃) (f₁ f₂ : M →L[R] M₂) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
@[simp]
theorem continuous_linear_map.add_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (g₁ g₂ : M₂ →L[R] M₃) (f : M →L[R] M₂) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem continuous_linear_map.comp_assoc {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (h : M₃ →L[R] M₄) (g : M₂ →L[R] M₃) (f : M →L[R] M₂) :
(h.comp g).comp f = h.comp (g.comp f)
@[instance]
def continuous_linear_map.has_mul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] :
Equations
theorem continuous_linear_map.mul_def {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (f g : M →L[R] M) :
f * g = f.comp g
@[simp]
theorem continuous_linear_map.coe_mul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (f g : M →L[R] M) :
f * g = f g
theorem continuous_linear_map.mul_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (f g : M →L[R] M) (x : M) :
(f * g) x = f (g x)
def continuous_linear_map.prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) :
M →L[R] M₂ × M₃

The cartesian product of two bounded linear maps, as a bounded linear map.

Equations
@[simp]
theorem continuous_linear_map.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) :
(f₁.prod f₂) = f₁.prod f₂
@[simp]
theorem continuous_linear_map.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) (x : M) :
(f₁.prod f₂) x = (f₁ x, f₂ x)
def continuous_linear_map.inl (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
M →L[R] M × M₂

The left injection into a product is a continuous linear map.

Equations
def continuous_linear_map.inr (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
M₂ →L[R] M × M₂

The right injection into a product is a continuous linear map.

Equations
@[simp]
theorem continuous_linear_map.inl_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (x : M) :
(continuous_linear_map.inl R M M₂) x = (x, 0)
@[simp]
theorem continuous_linear_map.inr_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (x : M₂) :
(continuous_linear_map.inr R M M₂) x = (0, x)
@[simp]
theorem continuous_linear_map.coe_inl {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.coe_inr {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
def continuous_linear_map.ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :

Kernel of a continuous linear map.

Equations
theorem continuous_linear_map.ker_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
@[simp]
theorem continuous_linear_map.mem_ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {f : M →L[R] M₂} {x : M} :
x f.ker f x = 0
theorem continuous_linear_map.is_closed_ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) [t1_space M₂] :
@[simp]
theorem continuous_linear_map.apply_ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (x : (f.ker)) :
f x = 0
theorem continuous_linear_map.is_complete_ker {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [module R M'] [t1_space M₂] (f : M' →L[R] M₂) :
@[instance]
def continuous_linear_map.complete_space_ker {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [module R M'] [t1_space M₂] (f : M' →L[R] M₂) :
@[simp]
theorem continuous_linear_map.ker_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :
(f.prod g).ker = f.ker g.ker
def continuous_linear_map.range {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
submodule R M₂

Range of a continuous linear map.

Equations
theorem continuous_linear_map.range_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) :
theorem continuous_linear_map.mem_range {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {f : M →L[R] M₂} {y : M₂} :
y f.range ∃ (x : M), f x = y
theorem continuous_linear_map.mem_range_self {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (x : M) :
theorem continuous_linear_map.range_prod_le {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :
def continuous_linear_map.cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ (x : M), f x p) :

Restrict codomain of a continuous linear map.

Equations
theorem continuous_linear_map.coe_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ (x : M), f x p) :
@[simp]
theorem continuous_linear_map.coe_cod_restrict_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ (x : M), f x p) (x : M) :
((f.cod_restrict p h) x) = f x
@[simp]
theorem continuous_linear_map.ker_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ (x : M), f x p) :
(f.cod_restrict p h).ker = f.ker
def continuous_linear_map.subtype_val {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (p : submodule R M) :

Embedding of a submodule into the ambient space as a continuous linear map.

Equations
@[simp]
theorem continuous_linear_map.subtype_val_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] (p : submodule R M) (x : p) :
def continuous_linear_map.fst (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
M × M₂ →L[R] M

prod.fst as a continuous_linear_map.

Equations
def continuous_linear_map.snd (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
M × M₂ →L[R] M₂

prod.snd as a continuous_linear_map.

Equations
@[simp]
theorem continuous_linear_map.coe_fst {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.coe_fst' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.coe_snd {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.coe_snd' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.fst_prod_snd {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_map.fst_comp_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :
(continuous_linear_map.fst R M₂ M₃).comp (f.prod g) = f
@[simp]
theorem continuous_linear_map.snd_comp_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :
(continuous_linear_map.snd R M₂ M₃).comp (f.prod g) = g
def continuous_linear_map.prod_map {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
M × M₃ →L[R] M₂ × M₄

prod.map of two continuous linear maps.

Equations
@[simp]
theorem continuous_linear_map.coe_prod_map {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
(f₁.prod_map f₂) = f₁.prod_map f₂
@[simp]
theorem continuous_linear_map.coe_prod_map' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
(f₁.prod_map f₂) = prod.map f₁ f₂
def continuous_linear_map.coprod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
M × M₂ →L[R] M₃

The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.

Equations
@[simp]
theorem continuous_linear_map.coe_coprod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
(f₁.coprod f₂) = f₁.coprod f₂
@[simp]
theorem continuous_linear_map.coprod_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) (x : M × M₂) :
(f₁.coprod f₂) x = f₁ x.fst + f₂ x.snd
theorem continuous_linear_map.range_coprod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
(f₁.coprod f₂).range = f₁.range f₂.range
def continuous_linear_map.smul_right {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {S : Type u_6} [semiring S] [module R S] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [has_continuous_smul S M₂] (c : M →L[R] S) (f : M₂) :
M →L[R] M₂

The linear map λ x, c x • f. Associates to a scalar-valued linear map and an element of M₂ the M₂-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂). See also continuous_linear_map.smul_rightₗ and continuous_linear_map.smul_rightL.

Equations
@[simp]
theorem continuous_linear_map.smul_right_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {S : Type u_6} [semiring S] [module R S] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [has_continuous_smul S M₂] {c : M →L[R] S} {f : M₂} {x : M} :
(c.smul_right f) x = c x f
@[simp]
theorem continuous_linear_map.smul_right_one_one {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] [topological_space R] [has_continuous_smul R M₂] (c : R →L[R] M₂) :
1.smul_right (c 1) = c
@[simp]
theorem continuous_linear_map.smul_right_one_eq_iff {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] [topological_space R] [has_continuous_smul R M₂] {f f' : M₂} :
1.smul_right f = 1.smul_right f' f = f'
theorem continuous_linear_map.smul_right_comp {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] [topological_space R] [has_continuous_smul R M₂] [has_continuous_mul R] {x : M₂} {c : R} :
def continuous_linear_map.pi {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
M →L[R] Π (i : ι), φ i

pi construction for continuous linear functions. From a family of continuous linear functions it produces a continuous linear function into a family of topological modules.

Equations
@[simp]
theorem continuous_linear_map.coe_pi' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
(continuous_linear_map.pi f) = λ (c : M) (i : ι), (f i) c
@[simp]
theorem continuous_linear_map.coe_pi {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
theorem continuous_linear_map.pi_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) (c : M) (i : ι) :
theorem continuous_linear_map.pi_eq_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
continuous_linear_map.pi f = 0 ∀ (i : ι), f i = 0
theorem continuous_linear_map.pi_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0
theorem continuous_linear_map.pi_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) (g : M₂ →L[R] M) :
def continuous_linear_map.proj {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (i : ι) :
(Π (i : ι), φ i) →L[R] φ i

The projections from a family of topological modules are continuous linear maps.

Equations
@[simp]
theorem continuous_linear_map.proj_apply {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (i : ι) (b : Π (i : ι), φ i) :
theorem continuous_linear_map.proj_pi {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M₂ →L[R] φ i) (i : ι) :
theorem continuous_linear_map.infi_ker_proj {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] :
(⨅ (i : ι), (continuous_linear_map.proj i).ker) =
def continuous_linear_map.infi_ker_proj_equiv (R : Type u_1) [semiring R] {ι : Type u_4} (φ : ι → Type u_5) [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] (hd : disjoint I J) (hu : set.univ I J) :
(⨅ (i : ι) (H : i J), (continuous_linear_map.proj i).ker) ≃L[R] Π (i : I), φ i

If I and J are complementary index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.

Equations
@[simp]
theorem continuous_linear_map.map_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (x : M) :
f (-x) = -f x
@[simp]
theorem continuous_linear_map.map_sub {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (x y : M) :
f (x - y) = f x - f y
@[simp]
theorem continuous_linear_map.sub_apply' {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) (x : M) :
(f - g) x = f x - g x
theorem continuous_linear_map.range_prod_eq {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₂] [module R M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} (h : f.ker g.ker = ) :
theorem continuous_linear_map.ker_prod_ker_le_ker_coprod {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
f.ker.prod g.ker (f.coprod g).ker
theorem continuous_linear_map.ker_coprod_of_disjoint_range {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) (hd : disjoint f.range g.range) :
(f.coprod g).ker = f.ker.prod g.ker
@[instance]
def continuous_linear_map.has_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M₂] :
has_neg (M →L[R] M₂)
Equations
@[simp]
theorem continuous_linear_map.neg_apply {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f : M →L[R] M₂) (x : M) [topological_add_group M₂] :
(-f) x = -f x
@[simp]
theorem continuous_linear_map.coe_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f : M →L[R] M₂) [topological_add_group M₂] :
theorem continuous_linear_map.coe_neg' {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f : M →L[R] M₂) [topological_add_group M₂] :
@[instance]
def continuous_linear_map.has_sub {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M₂] :
has_sub (M →L[R] M₂)
Equations
theorem continuous_linear_map.continuous_gsmul {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [topological_add_group M₂] (n : ) :
continuous (λ (x : M₂), n x)
theorem continuous_linear_map.continuous.gsmul {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [topological_add_group M₂] {α : Type u_1} [topological_space α] {n : } {f : α → M₂} (hf : continuous f) :
continuous (λ (x : α), n f x)
@[instance]
def continuous_linear_map.add_comm_group {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M₂] :
Equations
theorem continuous_linear_map.sub_apply {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) [topological_add_group M₂] (x : M) :
(f - g) x = f x - g x
@[simp]
theorem continuous_linear_map.coe_sub {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) [topological_add_group M₂] :
(f - g) = f - g
@[simp]
theorem continuous_linear_map.coe_sub' {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (f g : M →L[R] M₂) [topological_add_group M₂] :
(f - g) = f - g
theorem continuous_linear_map.smul_right_one_pow {R : Type u_1} [ring R] [topological_space R] [topological_ring R] (c : R) (n : ) :
1.smul_right c ^ n = 1.smul_right (c ^ n)
def continuous_linear_map.proj_ker_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) :
M →L[R] (f₁.ker)

Given a right inverse f₂ : M₂ →L[R] M to f₁ : M →L[R] M₂, proj_ker_of_right_inverse f₁ f₂ h is the projection M →L[R] f₁.ker along f₂.range.

Equations
@[simp]
theorem continuous_linear_map.coe_proj_ker_of_right_inverse_apply {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (x : M) :
((f₁.proj_ker_of_right_inverse f₂ h) x) = x - f₂ (f₁ x)
@[simp]
theorem continuous_linear_map.proj_ker_of_right_inverse_apply_idem {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (x : (f₁.ker)) :
@[simp]
theorem continuous_linear_map.proj_ker_of_right_inverse_comp_inv {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (y : M₂) :
(f₁.proj_ker_of_right_inverse f₂ h) (f₂ y) = 0
@[instance]
def continuous_linear_map.has_scalar {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] [module S M₃] [smul_comm_class R S M₃] [has_continuous_smul S M₃] :
has_scalar S (M →L[R] M₃)
Equations
@[simp]
theorem continuous_linear_map.smul_comp {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] [module S M₃] [smul_comm_class R S M₃] [has_continuous_smul S M₃] (c : S) (h : M₂ →L[R] M₃) (f : M →L[R] M₂) :
(c h).comp f = c h.comp f
theorem continuous_linear_map.smul_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] (c : S) (f : M →L[R] M₂) (x : M) [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] :
(c f) x = c f x
@[simp]
theorem continuous_linear_map.coe_smul {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] (c : S) (f : M →L[R] M₂) [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] :
(c f) = c f
@[simp]
theorem continuous_linear_map.coe_smul' {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] (c : S) (f : M →L[R] M₂) [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] :
(c f) = c f
@[simp]
theorem continuous_linear_map.comp_smul {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] [module S M₃] [smul_comm_class R S M₃] [has_continuous_smul S M₃] (c : S) (h : M₂ →L[R] M₃) (f : M →L[R] M₂) [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] [linear_map.compatible_smul M₂ M₃ S R] :
h.comp (c f) = c h.comp f
def continuous_linear_map.prod_equiv {R : Type u_1} [semiring R] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] :
(M →L[R] M₂) × (M →L[R] M₃) (M →L[R] M₂ × M₃)

continuous_linear_map.prod as an equiv.

Equations
@[simp]
theorem continuous_linear_map.prod_equiv_apply {R : Type u_1} [semiring R] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] (f : (M →L[R] M₂) × (M →L[R] M₃)) :
theorem continuous_linear_map.prod_ext_iff {R : Type u_1} [semiring R] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] {f g : M × M₂ →L[R] M₃} :
@[ext]
theorem continuous_linear_map.prod_ext {R : Type u_1} [semiring R] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] {f g : M × M₂ →L[R] M₃} (hl : f.comp (continuous_linear_map.inl R M M₂) = g.comp (continuous_linear_map.inl R M M₂)) (hr : f.comp (continuous_linear_map.inr R M M₂) = g.comp (continuous_linear_map.inr R M M₂)) :
f = g
@[instance]
def continuous_linear_map.module {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] [has_continuous_add M₂] :
module S (M →L[R] M₂)
Equations
@[simp]
theorem continuous_linear_map.prodₗ_apply {R : Type u_1} (S : Type u_2) [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] [module S M₃] [smul_comm_class R S M₃] [has_continuous_smul S M₃] [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] [has_continuous_add M₂] [has_continuous_add M₃] (ᾰ : (M →L[R] M₂) × (M →L[R] M₃)) :
def continuous_linear_map.prodₗ {R : Type u_1} (S : Type u_2) [semiring R] [semiring S] [topological_space S] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_5} [topological_space M₃] [add_comm_monoid M₃] [module R M₃] [module S M₃] [smul_comm_class R S M₃] [has_continuous_smul S M₃] [module S M₂] [has_continuous_smul S M₂] [smul_comm_class R S M₂] [has_continuous_add M₂] [has_continuous_add M₃] :
((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] M →L[R] M₂ × M₃

continuous_linear_map.prod as a linear_equiv.

Equations
def continuous_linear_map.smul_rightₗ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [ring R] [ring S] [ring T] [module R S] [add_comm_group M₂] [module R M₂] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [topological_space M₂] [has_continuous_smul S M₂] [topological_space M] [add_comm_group M] [module R M] [topological_add_group M₂] [topological_space T] [module T M₂] [has_continuous_smul T M₂] [smul_comm_class R T M₂] [smul_comm_class S T M₂] (c : M →L[R] S) :
M₂ →ₗ[T] M →L[R] M₂

Given c : E →L[𝕜] 𝕜, c.smul_rightₗ is the linear map from F to E →L[𝕜] F sending f to λ e, c e • f. See also continuous_linear_map.smul_rightL.

Equations
@[simp]
theorem continuous_linear_map.coe_smul_rightₗ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [ring R] [ring S] [ring T] [module R S] [add_comm_group M₂] [module R M₂] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [topological_space M₂] [has_continuous_smul S M₂] [topological_space M] [add_comm_group M] [module R M] [topological_add_group M₂] [topological_space T] [module T M₂] [has_continuous_smul T M₂] [smul_comm_class R T M₂] [smul_comm_class S T M₂] (c : M →L[R] S) :
@[instance]
def continuous_linear_map.algebra {R : Type u_1} [comm_ring R] [topological_space R] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_add_group M₂] [has_continuous_smul R M₂] :
algebra R (M₂ →L[R] M₂)
Equations
def continuous_linear_map.restrict_scalars {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] (R : Type u_4) [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (f : M →L[A] M₂) :
M →L[R] M₂

If A is an R-algebra, then a continuous A-linear map can be interpreted as a continuous R-linear map. We assume linear_map.compatible_smul M M₂ R A to match assumptions of linear_map.map_smul_of_tower.

Equations
@[simp]
theorem continuous_linear_map.coe_restrict_scalars {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (f : M →L[A] M₂) :
@[simp]
theorem continuous_linear_map.coe_restrict_scalars' {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (f : M →L[A] M₂) :
@[simp]
theorem continuous_linear_map.restrict_scalars_zero {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] :
@[simp]
theorem continuous_linear_map.restrict_scalars_add {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] [topological_add_group M₂] (f g : M →L[A] M₂) :
@[simp]
theorem continuous_linear_map.restrict_scalars_neg {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] [topological_add_group M₂] (f : M →L[A] M₂) :
@[simp]
theorem continuous_linear_map.restrict_scalars_smul {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] {S : Type u_5} [ring S] [topological_space S] [module S M₂] [has_continuous_smul S M₂] [smul_comm_class A S M₂] [smul_comm_class R S M₂] (c : S) (f : M →L[A] M₂) :
def continuous_linear_map.restrict_scalarsₗ (A : Type u_1) (M : Type u_2) (M₂ : Type u_3) [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] (R : Type u_4) [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (S : Type u_5) [ring S] [topological_space S] [module S M₂] [has_continuous_smul S M₂] [smul_comm_class A S M₂] [smul_comm_class R S M₂] [topological_add_group M₂] :
(M →L[A] M₂) →ₗ[S] M →L[R] M₂

continuous_linear_map.restrict_scalars as a linear_map. See also continuous_linear_map.restrict_scalarsL.

Equations
@[simp]
theorem continuous_linear_map.coe_restrict_scalarsₗ {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] {S : Type u_5} [ring S] [topological_space S] [module S M₂] [has_continuous_smul S M₂] [smul_comm_class A S M₂] [smul_comm_class R S M₂] [topological_add_group M₂] :
def continuous_linear_equiv.to_continuous_linear_map {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
M →L[R] M₂

A continuous linear equivalence induces a continuous linear map.

Equations
@[instance]
def continuous_linear_equiv.continuous_linear_map.has_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
has_coe (M ≃L[R] M₂) (M →L[R] M₂)

Coerce continuous linear equivs to continuous linear maps.

Equations
@[instance]
def continuous_linear_equiv.has_coe_to_fun {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :

Coerce continuous linear equivs to maps.

Equations
@[simp]
theorem continuous_linear_equiv.coe_def_rev {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.coe_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (b : M) :
e b = e b
@[simp]
theorem continuous_linear_equiv.coe_to_linear_equiv {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.coe_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
@[ext]
theorem continuous_linear_equiv.ext {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M ≃L[R] M₂} (h : f = g) :
f = g
theorem continuous_linear_equiv.coe_injective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem continuous_linear_equiv.coe_inj {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {e e' : M ≃L[R] M₂} :
e = e' e = e'
def continuous_linear_equiv.to_homeomorph {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
M ≃ₜ M₂

A continuous linear equivalence induces a homeomorphism.

Equations
@[simp]
theorem continuous_linear_equiv.coe_to_homeomorph {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.image_closure {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (s : set M) :
theorem continuous_linear_equiv.preimage_closure {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (s : set M₂) :
@[simp]
theorem continuous_linear_equiv.is_closed_image {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) {s : set M} :
theorem continuous_linear_equiv.map_nhds_eq {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (x : M) :
@[simp]
theorem continuous_linear_equiv.map_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
e 0 = 0
@[simp]
theorem continuous_linear_equiv.map_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (x y : M) :
e (x + y) = e x + e y
@[simp]
theorem continuous_linear_equiv.map_smul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (c : R) (x : M) :
e (c x) = c e x
@[simp]
theorem continuous_linear_equiv.map_eq_zero_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) {x : M} :
e x = 0 x = 0
theorem continuous_linear_equiv.continuous {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.continuous_on {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) {s : set M} :
theorem continuous_linear_equiv.continuous_at {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) {x : M} :
theorem continuous_linear_equiv.continuous_within_at {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) {s : set M} {x : M} :
theorem continuous_linear_equiv.comp_continuous_on_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {α : Type u_4} [topological_space α] (e : M ≃L[R] M₂) {f : α → M} {s : set α} :
theorem continuous_linear_equiv.comp_continuous_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] {α : Type u_4} [topological_space α] (e : M ≃L[R] M₂) {f : α → M} :
theorem continuous_linear_equiv.ext₁ {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] [topological_space R] {f g : R ≃L[R] M} (h : f 1 = g 1) :
f = g

An extensionality lemma for R ≃L[R] M.

def continuous_linear_equiv.refl (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] [module R M] :
M ≃L[R] M

The identity map as a continuous linear equivalence.

Equations
@[simp]
def continuous_linear_equiv.symm {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
M₂ ≃L[R] M

The inverse of a continuous linear equivalence as a continuous linear equivalence

Equations
@[simp]
theorem continuous_linear_equiv.symm_to_linear_equiv {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.symm_to_homeomorph {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.symm_map_nhds_eq {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) (x : M) :
def continuous_linear_equiv.trans {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) :
M ≃L[R] M₃

The composition of two continuous linear equivalences as a continuous linear equivalence.

Equations
@[simp]
theorem continuous_linear_equiv.trans_to_linear_equiv {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) :
def continuous_linear_equiv.prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) :
(M × M₃) ≃L[R] M₂ × M₄

Product of two continuous linear equivalences. The map comes from equiv.prod_congr.

Equations
@[simp]
theorem continuous_linear_equiv.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (x : M × M₃) :
(e.prod e') x = (e x.fst, e' x.snd)
@[simp]
theorem continuous_linear_equiv.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) :
theorem continuous_linear_equiv.bijective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.injective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃L[R