# mathlibdocumentation

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] [ M] [ M] [(𝓝[{x : R | is_unit x}] 0).ne_bot] (s : 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] [ M] [ M] (s : M) :
(λ (p : R × M), p.fst p.snd) '' set.univ.prod (closure s)
theorem submodule.closure_smul_self_eq {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
(λ (p : R × M), p.fst p.snd) '' set.univ.prod (closure s) =
def submodule.topological_closure {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
M

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

Equations
@[simp]
theorem submodule.topological_closure_coe {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
@[protected, instance]
def submodule.topological_closure_has_continuous_smul {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
theorem submodule.submodule_topological_closure {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
theorem submodule.is_closed_topological_closure {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
theorem submodule.topological_closure_minimal {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) {t : M} (h : s t) (ht : is_closed t) :
structure continuous_linear_map (R : Type u_1) [semiring R] (M : Type u_2) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_2 u_3)
• to_linear_map : M →ₗ[R] M₂
• cont : . "continuity'"

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) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_2 u_3)
• to_linear_equiv : M ≃ₗ[R] M₂
• continuous_to_fun : . "continuity'"
• continuous_inv_fun : . "continuity'"

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. #

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

Coerce continuous linear maps to linear maps.

Equations
@[protected, instance]
def continuous_linear_map.to_fun {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (h : . "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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (h : . "continuity'") :
@[protected, continuity]
theorem continuous_linear_map.continuous {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
theorem continuous_linear_map.coe_injective {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
@[simp, norm_cast]
theorem continuous_linear_map.coe_inj {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
function.injective (λ (f : M →L[R] M₂), show M → M₂, from f)
@[ext]
theorem continuous_linear_map.ext {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {R : Type u_1} {S : Type u_4} [semiring S] [ M] [ M] [ M₂] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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, norm_cast]
theorem continuous_linear_map.coe_coe {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
@[ext]
theorem continuous_linear_map.ext_ring {R : Type u_1} [semiring R] {M : Type u_2} [ M] {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} [ M] {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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] [t2_space M₂] {s : set M} {f g : M →L[R] M₂} (h : g s) :
g (closure 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] [t2_space M₂] {s : set M} (hs : dense s)) {f g : M →L[R] M₂} (h : 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.

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

The continuous map that is constantly zero.

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

the identity map as a continuous linear map.

Equations
@[protected, instance]
def continuous_linear_map.has_one {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
Equations
theorem continuous_linear_map.one_def {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
theorem continuous_linear_map.id_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] (x : M) :
x = x
@[simp, norm_cast]
theorem continuous_linear_map.coe_id {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
@[simp, norm_cast]
theorem continuous_linear_map.coe_id' {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
@[simp, norm_cast]
theorem continuous_linear_map.coe_eq_id {R : Type u_1} [semiring R] {M : Type u_2} [ M] {f : M →L[R] M} :
@[simp]
theorem continuous_linear_map.one_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] (x : M) :
1 x = x
@[protected, instance]
def continuous_linear_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂]  :
Equations
theorem continuous_linear_map.continuous_nsmul {M₂ : Type u_3} [add_comm_monoid M₂] (n : ) :
continuous (λ (x : M₂), n x)
@[continuity]
theorem continuous_linear_map.continuous.nsmul {M₂ : Type u_3} [add_comm_monoid M₂] {α : Type u_1} {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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f g : M →L[R] M₂) (x : M)  :
(f + g) x = f x + g x
@[simp, norm_cast]
theorem continuous_linear_map.coe_add {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f g : M →L[R] M₂)  :
(f + g) = f + g
@[norm_cast]
theorem continuous_linear_map.coe_add' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f g : M →L[R] M₂)  :
(f + g) = f + g
@[protected, instance]
def continuous_linear_map.add_comm_monoid {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂]  :
Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_sum {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {ι : Type u_4} (t : finset ι) (f : ι → (M →L[R] M₂)) :
∑ (d : ι) in t, f d = ∑ (d : ι) in t, (f d)
@[simp, norm_cast]
theorem continuous_linear_map.coe_sum' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (g : M₂ →L[R] M₃) (f : M →L[R] M₂) :
M →L[R] M₃

Composition of bounded linear maps.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_comp {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →L[R] M₂) (h : M₂ →L[R] M₃) :
(h.comp f) = h.comp f
@[simp, norm_cast]
theorem continuous_linear_map.coe_comp' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
f.comp = f
@[simp]
theorem continuous_linear_map.id_comp {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
M₂).comp f = f
@[simp]
theorem continuous_linear_map.comp_zero {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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)
@[protected, instance]
def continuous_linear_map.has_mul {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
Equations
theorem continuous_linear_map.mul_def {R : Type u_1} [semiring R] {M : Type u_2} [ 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} [ 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} [ M] (f g : M →L[R] M) (x : M) :
(f * g) x = f (g x)
@[protected]
def continuous_linear_map.prod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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, norm_cast]
theorem continuous_linear_map.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) :
(f₁.prod f₂) = f₁.prod f₂
@[simp, norm_cast]
theorem continuous_linear_map.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ 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) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (x : M) :
M₂) x = (x, 0)
@[simp]
theorem continuous_linear_map.inr_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (x : M₂) :
M₂) x = (0, x)
@[simp, norm_cast]
theorem continuous_linear_map.coe_inl {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_inr {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = M₂
def continuous_linear_map.ker {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
M

Kernel of a continuous linear map.

Equations
@[norm_cast]
theorem continuous_linear_map.ker_coe {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
@[simp]
theorem continuous_linear_map.mem_ker {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} [add_comm_monoid M₂] [ M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [ M'] [t1_space M₂] (f : M' →L[R] M₂) :
@[protected, instance]
def continuous_linear_map.complete_space_ker {R : Type u_1} [semiring R] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
M₂

Range of a continuous linear map.

Equations
theorem continuous_linear_map.range_coe {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
(f.range) =
theorem continuous_linear_map.mem_range {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : M₂) (h : ∀ (x : M), f x p) :

Restrict codomain of a continuous linear map.

Equations
@[norm_cast]
theorem continuous_linear_map.coe_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : 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} [ M] (p : M) :

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

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_subtype_val {R : Type u_1} [semiring R] {M : Type u_2} [ M] (p : M) :
@[simp, norm_cast]
theorem continuous_linear_map.subtype_val_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] (p : M) (x : p) :
def continuous_linear_map.fst (R : Type u_1) [semiring R] (M : Type u_2) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ 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) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ M₂] :
M × M₂ →L[R] M₂

`prod.snd` as a `continuous_linear_map`.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_fst {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_fst' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = prod.fst
@[simp, norm_cast]
theorem continuous_linear_map.coe_snd {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_snd' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = prod.snd
@[simp]
theorem continuous_linear_map.fst_prod_snd {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂).prod M₂) = (M × M₂)
@[simp]
theorem continuous_linear_map.fst_comp_prod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →L[R] M₂) (g : M →L[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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :
M₃).comp (f.prod g) = g
def continuous_linear_map.prod_map {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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, norm_cast]
theorem continuous_linear_map.coe_prod_map {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
(f₁.prod_map f₂) = f₁.prod_map f₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_prod_map' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
(f₁.prod_map f₂) = f₂
def continuous_linear_map.coprod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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, norm_cast]
theorem continuous_linear_map.coe_coprod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {S : Type u_6} [semiring S] [ S] [ M₂] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {S : Type u_6} [semiring S] [ S] [ M₂] [ M₂] [ 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} [add_comm_monoid M₂] [ M₂] [ 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} [add_comm_monoid M₂] [ M₂] [ 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} [add_comm_monoid M₂] [ M₂] [ M₂] {x : M₂} {c : R} :
def continuous_linear_map.pi {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
= λ (c : M) (i : ι), (f i) c
@[simp]
theorem continuous_linear_map.coe_pi {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
= linear_map.pi (λ (i : ι), (f i))
theorem continuous_linear_map.pi_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) (c : M) (i : ι) :
i = (f i) c
theorem continuous_linear_map.pi_eq_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
∀ (i : ι), f i = 0
theorem continuous_linear_map.pi_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0
theorem continuous_linear_map.pi_comp {R : Type u_1} [semiring R] {M : Type u_2} [ M] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) (g : M₂ →L[R] M) :
= continuous_linear_map.pi (λ (i : ι), (f i).comp g)
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 : ι), (φ 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 : ι), (φ i)] (i : ι) (b : Π (i : ι), φ i) :
= b i
theorem continuous_linear_map.proj_pi {R : Type u_1} [semiring R] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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 : ι), (φ i)] :
(⨅ (i : ι), =
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 : ι), (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] (hd : J) (hu : set.univ I J) :
(⨅ (i : ι) (H : i J), ≃L[R] Π (i : I), φ i

If `I` and `J` are complementary index sets, the product of the kernels of the `J`th 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_group M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_group M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M] [ M₂] [ M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) (hd : g.range) :
(f.coprod g).ker = f.ker.prod g.ker
@[protected, instance]
def continuous_linear_map.has_neg {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f : M →L[R] M₂) (x : M)  :
(-f) x = -f x
@[simp, norm_cast]
theorem continuous_linear_map.coe_neg {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f : M →L[R] M₂)  :
@[norm_cast]
theorem continuous_linear_map.coe_neg' {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f : M →L[R] M₂)  :
@[protected, instance]
def continuous_linear_map.has_sub {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂]  :
has_sub (M →L[R] M₂)
Equations
theorem continuous_linear_map.continuous_gsmul {M₂ : Type u_3} [add_comm_group M₂] (n : ) :
continuous (λ (x : M₂), n x)
@[continuity]
theorem continuous_linear_map.continuous.gsmul {M₂ : Type u_3} [add_comm_group M₂] {α : Type u_1} {n : } {f : α → M₂} (hf : continuous f) :
continuous (λ (x : α), n f x)
@[protected, instance]
def continuous_linear_map.add_comm_group {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂]  :
Equations
theorem continuous_linear_map.sub_apply {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f g : M →L[R] M₂) (x : M) :
(f - g) x = f x - g x
@[simp, norm_cast]
theorem continuous_linear_map.coe_sub {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f g : M →L[R] M₂)  :
(f - g) = f - g
@[simp, norm_cast]
theorem continuous_linear_map.coe_sub' {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f g : M →L[R] M₂)  :
(f - g) = f - g
@[protected, instance]
def continuous_linear_map.ring {R : Type u_1} [ring R] {M : Type u_2} [ M]  :
ring (M →L[R] M)
Equations
theorem continuous_linear_map.smul_right_one_pow {R : Type u_1} [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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (x : M) :
( 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (x : (f₁.ker)) :
h) x = x
@[simp]
theorem continuous_linear_map.proj_ker_of_right_inverse_comp_inv {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (y : M₂) :
h) (f₂ y) = 0
@[protected, instance]
def continuous_linear_map.has_scalar {R : Type u_1} {S : Type u_2} [ring R] [ring S] {M : Type u_3} [ M] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] [ M₃] [ M₃] [ M₃] :
(M →L[R] M₃)
Equations
@[simp]
theorem continuous_linear_map.smul_comp {R : Type u_1} {S : Type u_2} [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] [ M₃] [ M₃] [ 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} [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] (c : S) (f : M →L[R] M₂) (x : M) [ M₂] [ M₂] [ M₂] :
(c f) x = c f x
@[simp, norm_cast]
theorem continuous_linear_map.coe_smul {R : Type u_1} {S : Type u_2} [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] (c : S) (f : M →L[R] M₂) [ M₂] [ M₂] [ M₂] :
(c f) = c f
@[simp, norm_cast]
theorem continuous_linear_map.coe_smul' {R : Type u_1} {S : Type u_2} [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] (c : S) (f : M →L[R] M₂) [ M₂] [ M₂] [ M₂] :
(c f) = c f
@[simp]
theorem continuous_linear_map.comp_smul {R : Type u_1} {S : Type u_2} [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] [ M₃] [ M₃] [ M₃] (c : S) (h : M₂ →L[R] M₃) (f : M →L[R] M₂) [ M₂] [ M₂] [ M₂] [ S R] :
h.comp (c f) = c h.comp f
def continuous_linear_map.prod_equiv {R : Type u_1} [ring R] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ 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} [ring R] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] (f : (M →L[R] M₂) × (M →L[R] M₃)) :
theorem continuous_linear_map.prod_ext_iff {R : Type u_1} [ring R] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] {f g : M × M₂ →L[R] M₃} :
f = g f.comp M₂) = g.comp M₂) f.comp M₂) = g.comp M₂)
@[ext]
theorem continuous_linear_map.prod_ext {R : Type u_1} [ring R] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] {f g : M × M₂ →L[R] M₃} (hl : f.comp M₂) = g.comp M₂)) (hr : f.comp M₂) = g.comp M₂)) :
f = g
@[protected, instance]
def continuous_linear_map.module {R : Type u_1} {S : Type u_2} [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] [ M₂] [ M₂] [ M₂]  :
(M →L[R] M₂)
Equations
@[simp]
theorem continuous_linear_map.prodₗ_apply {R : Type u_1} (S : Type u_2) [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] [ M₃] [ M₃] [ M₃] [ M₂] [ M₂] [ M₂] (ᾰ : (M →L[R] M₂) × (M →L[R] M₃)) :
def continuous_linear_map.prodₗ {R : Type u_1} (S : Type u_2) [ring R] [ring S] {M : Type u_3} [ M] {M₂ : Type u_4} [add_comm_group M₂] [ M₂] {M₃ : Type u_5} [add_comm_group M₃] [ M₃] [ M₃] [ M₃] [ M₃] [ M₂] [ M₂] [ 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] [ S] [add_comm_group M₂] [ M₂] [ M₂] [ M₂] [ M₂] [ M] [ M₂] [ M₂] [ M₂] [ 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] [ S] [add_comm_group M₂] [ M₂] [ M₂] [ M₂] [ M₂] [ M] [ M₂] [ M₂] [ M₂] [ M₂] (c : M →L[R] S) :
@[protected, instance]
def continuous_linear_map.algebra {R : Type u_1} [comm_ring R] {M₂ : Type u_3} [add_comm_group M₂] [ M₂] [ M₂] :
(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₂] [ M] [ M₂] (R : Type u_4) [ring R] [ M] [ M₂] [ 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, norm_cast]
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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ 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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ 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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ 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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ A] (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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ A] (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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ A] {S : Type u_5} [ring S] [ M₂] [ M₂] [ M₂] [ 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₂] [ M] [ M₂] (R : Type u_4) [ring R] [ M] [ M₂] [ A] (S : Type u_5) [ring S] [ M₂] [ M₂] [ M₂] [ 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₂] [ M] [ M₂] {R : Type u_4} [ring R] [ M] [ M₂] [ A] {S : Type u_5} [ring S] [ M₂] [ M₂] [ M₂] [ M₂]  :
def continuous_linear_equiv.to_continuous_linear_map {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
M →L[R] M₂

A continuous linear equivalence induces a continuous linear map.

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

Coerce continuous linear equivs to continuous linear maps.

Equations
@[protected, instance]
def continuous_linear_equiv.has_coe_to_fun {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.coe_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M ≃L[R] M₂) :
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_coe {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.to_linear_equiv_injective {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
@[ext]
theorem continuous_linear_equiv.ext {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_inj {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.image_closure {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (x : M) :
(𝓝 x) = 𝓝 (e x)
@[simp]
theorem continuous_linear_equiv.map_zero {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) {x : M} :
e x = 0 x = 0
@[protected, continuity]
theorem continuous_linear_equiv.continuous {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[protected]
theorem continuous_linear_equiv.continuous_on {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) {s : set M} :
@[protected]
theorem continuous_linear_equiv.continuous_at {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) {x : M} :
@[protected]
theorem continuous_linear_equiv.continuous_within_at {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {α : Type u_4} (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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {α : Type u_4} (e : M ≃L[R] M₂) {f : α → M} :
theorem continuous_linear_equiv.ext₁ {R : Type u_1} [semiring R] {M : Type u_2} [ M] {f g : R ≃L[R] M} (h : f 1 = g 1) :
f = g

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

@[protected]
def continuous_linear_equiv.refl (R : Type u_1) [semiring R] (M : Type u_2) [ M] :
M ≃L[R] M

The identity map as a continuous linear equivalence.

Equations
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_refl {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_refl' {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
@[protected]
def continuous_linear_equiv.symm {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.symm_to_homeomorph {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.symm_map_nhds_eq {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (x : M) :
@[protected]
def continuous_linear_equiv.trans {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) :
(e₁.trans e₂).to_linear_equiv =
def continuous_linear_equiv.prod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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, norm_cast]
theorem continuous_linear_equiv.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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, norm_cast]
theorem continuous_linear_equiv.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.injective {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
theorem continuous_linear_equiv.surjective {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.trans_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) (c : M) :
(e₁.trans e₂) c = e₂ (e₁ c)
@[simp]
theorem continuous_linear_equiv.apply_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (c : M₂) :
e ((e.symm) c) = c
@[simp]
theorem continuous_linear_equiv.symm_apply_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (b : M) :
(e.symm) (e b) = b
@[simp]
theorem continuous_linear_equiv.symm_trans_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (e₁ : M₂ ≃L[R] M) (e₂ : M₃ ≃L[R] M₂) (c : M) :
((e₂.trans e₁).symm) c = (e₂.symm) ((e₁.symm) c)
@[simp]
theorem continuous_linear_equiv.symm_image_image {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (s : set M) :
(e.symm) '' (e '' s) = s
@[simp]
theorem continuous_linear_equiv.image_symm_image {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (s : set M₂) :
e '' ((e.symm) '' s) = s
@[simp, norm_cast]
theorem continuous_linear_equiv.comp_coe {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M ≃L[R] M₂) (f' : M₂ ≃L[R] M₃) :
f'.comp f = (f.trans f')
@[simp]
theorem continuous_linear_equiv.coe_comp_coe_symm {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.coe_symm_comp_coe {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.symm_comp_self {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.self_comp_symm {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
@[simp]
theorem continuous_linear_equiv.symm_symm {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :
e.symm.symm = e
@[simp]
theorem continuous_linear_equiv.refl_symm {R : Type u_1} [semiring R] {M : Type u_2} [ M] :
theorem continuous_linear_equiv.symm_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) (x : M) :
(e.symm.symm) x = e x