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 has_continuous_smul.of_nhds_zero {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_ring R] [topological_add_group M] (hmul : filter.tendsto (λ (p : R × M), p.fst p.snd) (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0)) (hmulleft : ∀ (m : M), filter.tendsto (λ (a : R), a m) (𝓝 0) (𝓝 0)) (hmulright : ∀ (a : R), filter.tendsto (λ (m : M), a m) (𝓝 0) (𝓝 0)) :
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] [has_continuous_add M] [module R M] [has_continuous_smul R 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.

Let R be a topological ring such that zero is not an isolated point (e.g., a nondiscrete normed field, see normed_field.punctured_nhds_ne_bot). Let M be a nontrivial module over R such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this using ne_bot (𝓝[{x}ᶜ] x).

This lemma is not an instance because Lean would need to find [has_continuous_smul ?m_1 M] with unknown ?m_1. We register this as an instance for R = ℝ in real.punctured_nhds_module_ne_bot. One can also use haveI := module.punctured_nhds_ne_bot R M in a proof.

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} {S : Type u_2} [semiring R] [semiring S] (σ : R →+* S) (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 S M₂] :
Type (max u_3 u_4)

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} {S : Type u_2} [semiring R] [semiring S] (σ : R →+* S) {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (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 S M₂] :
Type (max u_3 u_4)

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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
has_coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
@[instance]
def continuous_linear_map.to_fun {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
has_coe_to_fun (M₁ →SL[σ₁₂] M₂)

Coerce continuous linear maps to functions.

Equations
@[simp]
theorem continuous_linear_map.coe_mk {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →ₛₗ[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : continuous f.to_fun . "continuity'") :
theorem continuous_linear_map.continuous {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
theorem continuous_linear_map.coe_injective {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
@[simp]
theorem continuous_linear_map.coe_inj {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] {f g : M₁ →SL[σ₁₂] M₂} :
f = g f = g
theorem continuous_linear_map.coe_fn_injective {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
@[ext]
theorem continuous_linear_map.ext {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] {f g : M₁ →SL[σ₁₂] M₂} (h : ∀ (x : M₁), f x = g x) :
f = g
theorem continuous_linear_map.ext_iff {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] {f g : M₁ →SL[σ₁₂] M₂} :
f = g ∀ (x : M₁), f x = g x
@[simp]
theorem continuous_linear_map.map_zero {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
f 0 = 0
@[simp]
theorem continuous_linear_map.map_add {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) (x y : M₁) :
f (x + y) = f x + f y
@[simp]
theorem continuous_linear_map.map_smulₛₗ {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) :
f (c x) = σ₁₂ c f x
@[simp]
theorem continuous_linear_map.map_smul {R₁ : Type u_1} [semiring R₁] {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₂] (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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) {ι : Type u_3} (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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
@[ext]
theorem continuous_linear_map.ext_ring {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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_4} [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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [t2_space M₂] {s : set M₁} {f g : M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [t2_space M₂] {s : set M₁} (hs : dense (submodule.span R₁ s)) {f g : M₁ →SL[σ₁₂] 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.

theorem submodule.topological_closure_map {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [ring_hom_surjective σ₁₂] [topological_space R₁] [topological_space R₂] [has_continuous_smul R₁ M₁] [has_continuous_add M₁] [has_continuous_smul R₂ M₂] [has_continuous_add M₂] (f : M₁ →SL[σ₁₂] M₂) (s : submodule R₁ M₁) :

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

theorem dense_range.topological_closure_map_submodule {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [ring_hom_surjective σ₁₂] [topological_space R₁] [topological_space R₂] [has_continuous_smul R₁ M₁] [has_continuous_add M₁] [has_continuous_smul R₂ M₂] [has_continuous_add M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : dense_range f) {s : submodule R₁ M₁} (hs : s.topological_closure = ) :

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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
has_zero (M₁ →SL[σ₁₂] M₂)

The continuous map that is constantly zero.

Equations
@[instance]
def continuous_linear_map.inhabited {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
inhabited (M₁ →SL[σ₁₂] M₂)
Equations
@[simp]
theorem continuous_linear_map.default_def {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
default (M₁ →SL[σ₁₂] M₂) = 0
@[simp]
theorem continuous_linear_map.zero_apply {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (x : M₁) :
0 x = 0
@[simp]
theorem continuous_linear_map.coe_zero {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
0 = 0
theorem continuous_linear_map.coe_zero' {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] :
0 = 0
@[instance]
def continuous_linear_map.unique_of_left {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [subsingleton M₁] :
unique (M₁ →SL[σ₁₂] M₂)
Equations
@[instance]
def continuous_linear_map.unique_of_right {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [subsingleton M₂] :
unique (M₁ →SL[σ₁₂] M₂)
Equations
def continuous_linear_map.id (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [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_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
has_one (M₁ →L[R₁] M₁)
Equations
theorem continuous_linear_map.one_def {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (x : M₁) :
@[simp]
theorem continuous_linear_map.coe_id {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
@[simp]
theorem continuous_linear_map.coe_id' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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_4} [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_4} [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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [has_continuous_add M₂] :
has_add (M₁ →SL[σ₁₂] M₂)
Equations
theorem continuous_linear_map.continuous_nsmul {M₂ : Type u_5} [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_5} [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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f g : M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f g : M₁ →SL[σ₁₂] M₂) [has_continuous_add M₂] :
(f + g) = f + g
theorem continuous_linear_map.coe_add' {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f g : M₁ →SL[σ₁₂] M₂) [has_continuous_add M₂] :
(f + g) = f + g
@[instance]
def continuous_linear_map.add_comm_monoid {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [has_continuous_add M₂] :
add_comm_monoid (M₁ →SL[σ₁₂] M₂)
Equations
@[simp]
theorem continuous_linear_map.coe_sum {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [has_continuous_add M₂] {ι : Type u_3} (t : finset ι) (f : ι → (M₁ →SL[σ₁₂] M₂)) :
∑ (d : ι) in t, f d = ∑ (d : ι) in t, (f d)
@[simp]
theorem continuous_linear_map.coe_sum' {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [has_continuous_add M₂] {ι : Type u_3} (t : finset ι) (f : ι → (M₁ →SL[σ₁₂] M₂)) :
∑ (d : ι) in t, f d = ∑ (d : ι) in t, (f d)
theorem continuous_linear_map.sum_apply {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [has_continuous_add M₂] {ι : Type u_3} (t : finset ι) (f : ι → (M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
M₁ →SL[σ₁₃] M₃

Composition of bounded linear maps.

Equations
@[simp]
theorem continuous_linear_map.coe_comp {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] (f : M₁ →SL[σ₁₂] M₂) (h : M₂ →SL[σ₂₃] M₃) {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] :
(h.comp f) = h.comp f
@[simp]
theorem continuous_linear_map.coe_comp' {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] (f : M₁ →SL[σ₁₂] M₂) (h : M₂ →SL[σ₂₃] M₃) {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] :
(h.comp f) = h f
theorem continuous_linear_map.comp_apply {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(g.comp f) x = g (f x)
@[simp]
theorem continuous_linear_map.comp_id {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_map.id_comp {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_map.comp_zero {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) :
g.comp 0 = 0
@[simp]
theorem continuous_linear_map.zero_comp {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] (f : M₁ →SL[σ₁₂] M₂) {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] :
0.comp f = 0
@[simp]
theorem continuous_linear_map.comp_add {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [has_continuous_add M₂] [has_continuous_add M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M₁ →SL[σ₁₂] M₂) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
@[simp]
theorem continuous_linear_map.add_comp {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [has_continuous_add M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem continuous_linear_map.comp_assoc {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {R₃ : Type u_3} [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_7} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_8} [semiring R₄] [module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄) (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] 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_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
has_mul (M₁ →L[R₁] M₁)
Equations
theorem continuous_linear_map.mul_def {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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_4} [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_4} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_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₂] :
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_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₂] :
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_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₂] (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_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₂] (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_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₂] :
(continuous_linear_map.inl R₁ M₁ M₂) = linear_map.inl R₁ M₁ M₂
@[simp]
theorem continuous_linear_map.coe_inr {R₁ : Type u_1} [semiring R₁] {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₂] :
(continuous_linear_map.inr R₁ M₁ M₂) = linear_map.inr R₁ M₁ M₂
def continuous_linear_map.ker {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
submodule R₁ M₁

Kernel of a continuous linear map.

Equations
theorem continuous_linear_map.ker_coe {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_map.mem_ker {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] {f : M₁ →SL[σ₁₂] M₂} {x : M₁} :
x f.ker f x = 0
theorem continuous_linear_map.is_closed_ker {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) [t1_space M₂] :
@[simp]
theorem continuous_linear_map.apply_ker {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) (x : (f.ker)) :
f x = 0
theorem continuous_linear_map.is_complete_ker {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {M' : Type u_3} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [module R₁ M'] [t1_space M₂] (f : M' →SL[σ₁₂] M₂) :
@[instance]
def continuous_linear_map.complete_space_ker {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {M' : Type u_3} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [module R₁ M'] [t1_space M₂] (f : M' →SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_map.ker_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [ring_hom_surjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :
submodule R₂ M₂

Range of a continuous linear map.

Equations
theorem continuous_linear_map.range_coe {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) [ring_hom_surjective σ₁₂] :
theorem continuous_linear_map.mem_range {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [ring_hom_surjective σ₁₂] {f : M₁ →SL[σ₁₂] M₂} {y : M₂} :
y f.range ∃ (x : M₁), f x = y
theorem continuous_linear_map.mem_range_self {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] [ring_hom_surjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :
theorem continuous_linear_map.range_prod_le {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] M₂) (p : submodule R₂ M₂) (h : ∀ (x : M₁), f x p) :
M₁ →SL[σ₁₂] p

Restrict codomain of a continuous linear map.

Equations
theorem continuous_linear_map.coe_cod_restrict {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {σ₁₂ : R₁ →+* R₂} {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₂] (f : M₁ →SL[σ₁₂] 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_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
p →L[R₁] M₁

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

Equations
@[simp]
theorem continuous_linear_map.coe_subtype_val {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
@[simp]
theorem continuous_linear_map.subtype_val_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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_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₂] :
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_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₂] :
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_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₂] :
(continuous_linear_map.fst R₁ M₁ M₂) = linear_map.fst R₁ M₁ M₂
@[simp]
theorem continuous_linear_map.coe_fst' {R₁ : Type u_1} [semiring R₁] {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₂] :
@[simp]
theorem continuous_linear_map.coe_snd {R₁ : Type u_1} [semiring R₁] {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₂] :
(continuous_linear_map.snd R₁ M₁ M₂) = linear_map.snd R₁ M₁ M₂
@[simp]
theorem continuous_linear_map.coe_snd' {R₁ : Type u_1} [semiring R₁] {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₂] :
@[simp]
theorem continuous_linear_map.fst_prod_snd {R₁ : Type u_1} [semiring R₁] {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₂] :
(continuous_linear_map.fst R₁ M₁ M₂).prod (continuous_linear_map.snd R₁ M₁ M₂) = continuous_linear_map.id R₁ (M₁ × M₂)
@[simp]
theorem continuous_linear_map.fst_comp_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_7} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_7} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_7} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_6} [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 {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_8} {S : Type u_9} [semiring R] [semiring S] [module R M₁] [module R M₂] [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 {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_5} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_8} {S : Type u_9} [semiring R] [semiring S] [module R M₁] [module R M₂] [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_5} [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_5} [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_5} [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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M) :
f (-x) = -f x
@[simp]
theorem continuous_linear_map.map_sub {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x y : M) :
f (x - y) = f x - f y
@[simp]
theorem continuous_linear_map.sub_apply' {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} (f g : M →SL[σ₁₂] 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_3} [topological_space M] [add_comm_group M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_5} [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_3} [topological_space M] [add_comm_group M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_5} [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_3} [topological_space M] [add_comm_group M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_5} [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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] :
has_neg (M →SL[σ₁₂] M₂)
Equations
@[simp]
theorem continuous_linear_map.neg_apply {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] (f : M →SL[σ₁₂] M₂) (x : M) :
(-f) x = -f x
@[simp]
theorem continuous_linear_map.coe_neg {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] (f : M →SL[σ₁₂] M₂) :
theorem continuous_linear_map.coe_neg' {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] (f : M →SL[σ₁₂] M₂) :
@[instance]
def continuous_linear_map.has_sub {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] :
has_sub (M →SL[σ₁₂] M₂)
Equations
theorem continuous_linear_map.continuous_gsmul {M₂ : Type u_4} [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_4} [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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] :
add_comm_group (M →SL[σ₁₂] M₂)
Equations
theorem continuous_linear_map.sub_apply {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] (f g : M →SL[σ₁₂] M₂) (x : M) :
(f - g) x = f x - g x
@[simp]
theorem continuous_linear_map.coe_sub {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] (f g : M →SL[σ₁₂] M₂) :
(f - g) = f - g
@[simp]
theorem continuous_linear_map.coe_sub' {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} [topological_add_group M₂] (f g : M →SL[σ₁₂] 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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] 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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] 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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] 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] {R₂ : Type u_2} [ring R₂] {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₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] 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₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) :
M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
has_coe (M₁ ≃SL[σ₁₂] M₂) (M₁ →SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
has_coe_to_fun (M₁ ≃SL[σ₁₂] M₂)

Coerce continuous linear equivs to maps.

Equations
@[simp]
theorem continuous_linear_equiv.coe_def_rev {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) :
theorem continuous_linear_equiv.coe_apply {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) :
e b = e b
@[simp]
theorem continuous_linear_equiv.coe_to_linear_equiv {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (f : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_equiv.coe_coe {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) :
theorem continuous_linear_equiv.to_linear_equiv_injective {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
@[ext]
theorem continuous_linear_equiv.ext {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {f g : M₁ ≃SL[σ₁₂] M₂} (h : f = g) :
f = g
theorem continuous_linear_equiv.coe_injective {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
@[simp]
theorem continuous_linear_equiv.coe_inj {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {e e' : M₁ ≃SL[σ₁₂] M₂} :
e = e' e = e'
def continuous_linear_equiv.to_homeomorph {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] 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₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) :
theorem continuous_linear_equiv.image_closure {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₁) :
theorem continuous_linear_equiv.preimage_closure {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) :
@[simp]
theorem continuous_linear_equiv.is_closed_image {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : set M₁} :
theorem continuous_linear_equiv.map_nhds_eq {R₁ : Type u_1} [semiring R₁] {R₂ : Type u_2} [semiring R₂] {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₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :
@[simp]
theorem