Theory of topological modules and continuous linear maps. #
We use the class has_continuous_smul for topological (semi) modules and topological vector spaces.
In this file we define continuous linear maps, as linear maps between topological modules which are
continuous. The set of continuous linear maps between the topological R-modules M and M₂ is
denoted by M →L[R] M₂.
Continuous linear equivalences are denoted by M ≃L[R] M₂.
theorem
submodule.eq_top_of_nonempty_interior'
{R : Type u_1}
{M : Type u_2}
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
[(𝓝[{x : R | is_unit x}] 0).ne_bot]
(s : submodule R M)
(hs : (interior ↑s).nonempty) :
If M is a topological module over R and 0 is a limit of invertible elements of R, then
⊤ is the only submodule of M with a nonempty interior.
This is the case, e.g., if R is a nondiscrete normed field.
theorem
submodule.closure_smul_self_subset
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
(s : submodule R M) :
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) :
def
submodule.topological_closure
{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]
[has_continuous_add M]
(s : submodule R M) :
submodule R M
The (topological-space) closure of a submodule of a topological R-module M is itself
a submodule.
@[simp]
theorem
submodule.topological_closure_coe
{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]
[has_continuous_add M]
(s : submodule R M) :
↑(s.topological_closure) = closure ↑s
@[protected, instance]
def
submodule.topological_closure_has_continuous_smul
{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]
[has_continuous_add M]
(s : submodule R M) :
theorem
submodule.submodule_topological_closure
{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]
[has_continuous_add M]
(s : submodule R M) :
s ≤ s.topological_closure
theorem
submodule.is_closed_topological_closure
{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]
[has_continuous_add M]
(s : submodule R M) :
theorem
submodule.topological_closure_minimal
{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]
[has_continuous_add M]
(s : submodule R M)
{t : submodule R M}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
structure
continuous_linear_map
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_3)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Type (max u_2 u_3)
- to_linear_map : M →ₗ[R] M₂
- cont : continuous c.to_linear_map.to_fun . "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)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_3)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Type (max u_2 u_3)
- to_linear_equiv : M ≃ₗ[R] M₂
- continuous_to_fun : continuous c.to_linear_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous c.to_linear_equiv.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}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Coerce continuous linear maps to linear maps.
Equations
@[protected, instance]
def
continuous_linear_map.to_fun
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
has_coe_to_fun (M →L[R] M₂)
Coerce continuous linear maps to functions.
@[simp]
theorem
continuous_linear_map.coe_mk
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(h : continuous f.to_fun . "continuity'") :
↑{to_linear_map := f, cont := h} = f
@[simp]
theorem
continuous_linear_map.coe_mk'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(h : continuous f.to_fun . "continuity'") :
@[protected, continuity]
theorem
continuous_linear_map.continuous
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
theorem
continuous_linear_map.coe_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inj
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f g : M →L[R] M₂} :
theorem
continuous_linear_map.coe_fn_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
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}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f g : M →L[R] M₂}
(h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
theorem
continuous_linear_map.ext_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f g : M →L[R] M₂} :
@[simp]
theorem
continuous_linear_map.map_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
@[simp]
theorem
continuous_linear_map.map_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_map.map_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(c : R)
(x : M) :
@[simp]
theorem
continuous_linear_map.map_smul_of_tower
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_1}
{S : Type u_4}
[semiring S]
[has_scalar R M]
[module S M]
[has_scalar R M₂]
[module S M₂]
[linear_map.compatible_smul M M₂ R S]
(f : M →L[S] M₂)
(c : R)
(x : M) :
theorem
continuous_linear_map.map_sum
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
{ι : Type u_4}
(s : finset ι)
(g : ι → M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
@[ext]
theorem
continuous_linear_map.ext_ring
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
[topological_space R]
{f g : R →L[R] M}
(h : ⇑f 1 = ⇑g 1) :
f = g
theorem
continuous_linear_map.ext_ring_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
[topological_space R]
{f g : R →L[R] M} :
theorem
continuous_linear_map.eq_on_closure_span
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[t2_space M₂]
{s : set M}
{f g : M →L[R] M₂}
(h : set.eq_on ⇑f ⇑g s) :
If two continuous linear maps are equal on a set s, then they are equal on the closure
of the submodule.span of this set.
theorem
continuous_linear_map.ext_on
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[t2_space M₂]
{s : set M}
(hs : dense ↑(submodule.span R s))
{f g : M →L[R] M₂}
(h : set.eq_on ⇑f ⇑g s) :
f = g
If the submodule generated by a set s is dense in the ambient module, then two continuous
linear maps equal on s are equal.
@[protected, instance]
def
continuous_linear_map.has_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
The continuous map that is constantly zero.
Equations
- continuous_linear_map.has_zero = {zero := {to_linear_map := 0, cont := _}}
@[protected, instance]
def
continuous_linear_map.inhabited
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Equations
@[simp]
theorem
continuous_linear_map.default_def
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
@[simp]
theorem
continuous_linear_map.zero_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
@[norm_cast]
theorem
continuous_linear_map.coe_zero'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
@[protected, instance]
def
continuous_linear_map.unique_of_left
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[subsingleton M] :
@[protected, instance]
def
continuous_linear_map.unique_of_right
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[subsingleton M₂] :
def
continuous_linear_map.id
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
[module R M] :
the identity map as a continuous linear map.
Equations
- continuous_linear_map.id R M = {to_linear_map := linear_map.id _inst_10, cont := _}
@[protected, instance]
def
continuous_linear_map.has_one
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
Equations
- continuous_linear_map.has_one = {one := continuous_linear_map.id R M _inst_10}
theorem
continuous_linear_map.one_def
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
1 = continuous_linear_map.id R M
theorem
continuous_linear_map.id_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(x : M) :
⇑(continuous_linear_map.id R M) x = x
@[simp, norm_cast]
theorem
continuous_linear_map.coe_id
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_id'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
⇑(continuous_linear_map.id R M) = id
@[simp, norm_cast]
theorem
continuous_linear_map.coe_eq_id
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{f : M →L[R] M} :
↑f = linear_map.id ↔ f = continuous_linear_map.id R M
@[simp]
theorem
continuous_linear_map.one_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(x : M) :
@[protected, instance]
def
continuous_linear_map.has_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[has_continuous_add M₂] :
theorem
continuous_linear_map.continuous_nsmul
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[has_continuous_add M₂]
(n : ℕ) :
continuous (λ (x : M₂), n • x)
@[continuity]
theorem
continuous_linear_map.continuous.nsmul
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[has_continuous_add M₂]
{α : Type u_1}
[topological_space α]
{n : ℕ}
{f : α → M₂}
(hf : continuous f) :
continuous (λ (x : α), n • f x)
@[simp]
theorem
continuous_linear_map.add_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
(x : M)
[has_continuous_add M₂] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
[has_continuous_add M₂] :
@[norm_cast]
theorem
continuous_linear_map.coe_add'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
[has_continuous_add M₂] :
@[protected, instance]
def
continuous_linear_map.add_comm_monoid
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[has_continuous_add M₂] :
add_comm_monoid (M →L[R] M₂)
Equations
- continuous_linear_map.add_comm_monoid = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (f : M →L[R] M₂), {to_linear_map := {to_fun := λ (x : M), n • ⇑f x, map_add' := _, map_smul' := _}, cont := _}, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sum
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[has_continuous_add M₂]
{ι : Type u_4}
(t : finset ι)
(f : ι → (M →L[R] M₂)) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sum'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[has_continuous_add M₂]
{ι : Type u_4}
(t : finset ι)
(f : ι → (M →L[R] M₂)) :
theorem
continuous_linear_map.sum_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[has_continuous_add M₂]
{ι : Type u_4}
(t : finset ι)
(f : ι → (M →L[R] M₂))
(b : M) :
def
continuous_linear_map.comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(g : M₂ →L[R] M₃)
(f : M →L[R] M₂) :
Composition of bounded linear maps.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂)
(h : M₂ →L[R] M₃) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_comp'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂)
(h : M₂ →L[R] M₃) :
@[simp]
theorem
continuous_linear_map.comp_id
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
f.comp (continuous_linear_map.id R M) = f
@[simp]
theorem
continuous_linear_map.id_comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
(continuous_linear_map.id R M₂).comp f = f
@[simp]
theorem
continuous_linear_map.comp_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂) :
@[simp]
theorem
continuous_linear_map.zero_comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂) :
@[simp]
theorem
continuous_linear_map.comp_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₂]
[has_continuous_add M₃]
(g : M₂ →L[R] M₃)
(f₁ f₂ : M →L[R] M₂) :
@[simp]
theorem
continuous_linear_map.add_comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(g₁ g₂ : M₂ →L[R] M₃)
(f : M →L[R] M₂) :
theorem
continuous_linear_map.comp_assoc
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(h : M₃ →L[R] M₄)
(g : M₂ →L[R] M₃)
(f : M →L[R] M₂) :
@[protected, instance]
def
continuous_linear_map.has_mul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
Equations
- continuous_linear_map.has_mul = {mul := continuous_linear_map.comp _inst_10}
theorem
continuous_linear_map.mul_def
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(f g : M →L[R] M) :
@[simp]
theorem
continuous_linear_map.coe_mul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(f g : M →L[R] M) :
theorem
continuous_linear_map.mul_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(f g : M →L[R] M)
(x : M) :
@[protected]
def
continuous_linear_map.prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f₁ : M →L[R] M₂)
(f₂ : M →L[R] M₃) :
The cartesian product of two bounded linear maps, as a bounded linear map.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f₁ : M →L[R] M₂)
(f₂ : M →L[R] M₃) :
@[simp, norm_cast]
theorem
continuous_linear_map.prod_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f₁ : M →L[R] M₂)
(f₂ : M →L[R] M₃)
(x : M) :
def
continuous_linear_map.inl
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_3)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
The left injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inl R M M₂ = (continuous_linear_map.id R M).prod 0
def
continuous_linear_map.inr
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_3)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
The right injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inr R M M₂ = 0.prod (continuous_linear_map.id R M₂)
@[simp]
theorem
continuous_linear_map.inl_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : M) :
⇑(continuous_linear_map.inl R M M₂) x = (x, 0)
@[simp]
theorem
continuous_linear_map.inr_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : M₂) :
⇑(continuous_linear_map.inr R M M₂) x = (0, x)
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inl
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
↑(continuous_linear_map.inl R M M₂) = linear_map.inl R M M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inr
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
↑(continuous_linear_map.inr R M M₂) = linear_map.inr R M M₂
def
continuous_linear_map.ker
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
submodule R M
Kernel of a continuous linear map.
@[norm_cast]
theorem
continuous_linear_map.ker_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
@[simp]
theorem
continuous_linear_map.mem_ker
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f : M →L[R] M₂}
{x : M} :
theorem
continuous_linear_map.is_closed_ker
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
[t1_space M₂] :
@[simp]
theorem
continuous_linear_map.apply_ker
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(x : ↥(f.ker)) :
theorem
continuous_linear_map.is_complete_ker
{R : Type u_1}
[semiring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
{M' : Type u_2}
[uniform_space M']
[complete_space M']
[add_comm_monoid M']
[module R M']
[t1_space M₂]
(f : M' →L[R] M₂) :
is_complete ↑(f.ker)
@[protected, instance]
def
continuous_linear_map.complete_space_ker
{R : Type u_1}
[semiring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
{M' : Type u_2}
[uniform_space M']
[complete_space M']
[add_comm_monoid M']
[module R M']
[t1_space M₂]
(f : M' →L[R] M₂) :
complete_space ↥(f.ker)
@[simp]
theorem
continuous_linear_map.ker_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂)
(g : M →L[R] M₃) :
def
continuous_linear_map.range
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
submodule R M₂
Range of a continuous linear map.
theorem
continuous_linear_map.range_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂) :
theorem
continuous_linear_map.mem_range
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f : M →L[R] M₂}
{y : M₂} :
theorem
continuous_linear_map.mem_range_self
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(x : M) :
theorem
continuous_linear_map.range_prod_le
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂)
(g : M →L[R] M₃) :
def
continuous_linear_map.cod_restrict
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(p : submodule R M₂)
(h : ∀ (x : M), ⇑f x ∈ p) :
Restrict codomain of a continuous linear map.
Equations
- f.cod_restrict p h = {to_linear_map := linear_map.cod_restrict p ↑f h, cont := _}
@[norm_cast]
theorem
continuous_linear_map.coe_cod_restrict
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(p : submodule R M₂)
(h : ∀ (x : M), ⇑f x ∈ p) :
↑(f.cod_restrict p h) = linear_map.cod_restrict p ↑f h
@[simp]
theorem
continuous_linear_map.coe_cod_restrict_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(p : submodule R M₂)
(h : ∀ (x : M), ⇑f x ∈ p)
(x : M) :
↑(⇑(f.cod_restrict p h) x) = ⇑f x
@[simp]
theorem
continuous_linear_map.ker_cod_restrict
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(p : submodule R M₂)
(h : ∀ (x : M), ⇑f x ∈ p) :
(f.cod_restrict p h).ker = f.ker
def
continuous_linear_map.subtype_val
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(p : submodule R M) :
Embedding of a submodule into the ambient space as a continuous linear map.
Equations
- continuous_linear_map.subtype_val p = {to_linear_map := p.subtype, cont := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_subtype_val
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(p : submodule R M) :
@[simp, norm_cast]
theorem
continuous_linear_map.subtype_val_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
(x : ↥p) :
⇑(continuous_linear_map.subtype_val p) x = ↑x
def
continuous_linear_map.fst
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_3)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
prod.fst as a continuous_linear_map.
Equations
- continuous_linear_map.fst R M M₂ = {to_linear_map := linear_map.fst R M M₂ _inst_11, cont := _}
def
continuous_linear_map.snd
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_3)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
prod.snd as a continuous_linear_map.
Equations
- continuous_linear_map.snd R M M₂ = {to_linear_map := linear_map.snd R M M₂ _inst_11, cont := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_fst
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
↑(continuous_linear_map.fst R M M₂) = linear_map.fst R M M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_fst'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
⇑(continuous_linear_map.fst R M M₂) = prod.fst
@[simp, norm_cast]
theorem
continuous_linear_map.coe_snd
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
↑(continuous_linear_map.snd R M M₂) = linear_map.snd R M M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_snd'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
⇑(continuous_linear_map.snd R M M₂) = prod.snd
@[simp]
theorem
continuous_linear_map.fst_prod_snd
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(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_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂)
(g : M →L[R] M₃) :
(continuous_linear_map.fst R M₂ M₃).comp (f.prod g) = f
@[simp]
theorem
continuous_linear_map.snd_comp_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →L[R] M₂)
(g : M →L[R] M₃) :
(continuous_linear_map.snd R M₂ M₃).comp (f.prod g) = g
def
continuous_linear_map.prod_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f₁ : M →L[R] M₂)
(f₂ : M₃ →L[R] M₄) :
prod.map of two continuous linear maps.
Equations
- f₁.prod_map f₂ = (f₁.comp (continuous_linear_map.fst R M M₃)).prod (f₂.comp (continuous_linear_map.snd R M M₃))
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f₁ : M →L[R] M₂)
(f₂ : M₃ →L[R] M₄) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod_map'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f₁ : M →L[R] M₂)
(f₂ : M₃ →L[R] M₄) :
def
continuous_linear_map.coprod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f₁ : M →L[R] M₃)
(f₂ : M₂ →L[R] M₃) :
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_coprod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f₁ : M →L[R] M₃)
(f₂ : M₂ →L[R] M₃) :
@[simp]
theorem
continuous_linear_map.coprod_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f₁ : M →L[R] M₃)
(f₂ : M₂ →L[R] M₃)
(x : M × M₂) :
theorem
continuous_linear_map.range_coprod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f₁ : M →L[R] M₃)
(f₂ : M₂ →L[R] M₃) :
def
continuous_linear_map.smul_right
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{S : Type u_6}
[semiring S]
[module R S]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[has_continuous_smul S M₂]
(c : M →L[R] S)
(f : M₂) :
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
- c.smul_right f = {to_linear_map := {to_fun := (c.to_linear_map.smul_right f).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_linear_map.smul_right_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{S : Type u_6}
[semiring S]
[module R S]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[has_continuous_smul S M₂]
{c : M →L[R] S}
{f : M₂}
{x : M} :
⇑(c.smul_right f) x = ⇑c x • f
@[simp]
theorem
continuous_linear_map.smul_right_one_one
{R : Type u_1}
[semiring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
[topological_space R]
[has_continuous_smul R M₂]
(c : R →L[R] M₂) :
1.smul_right (⇑c 1) = c
@[simp]
theorem
continuous_linear_map.smul_right_one_eq_iff
{R : Type u_1}
[semiring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
[topological_space R]
[has_continuous_smul R M₂]
{f f' : M₂} :
1.smul_right f = 1.smul_right f' ↔ f = f'
theorem
continuous_linear_map.smul_right_comp
{R : Type u_1}
[semiring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
[topological_space R]
[has_continuous_smul R M₂]
[has_continuous_mul R]
{x : M₂}
{c : R} :
(1.smul_right x).comp (1.smul_right c) = 1.smul_right (c • x)
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) :
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
- continuous_linear_map.pi f = {to_linear_map := linear_map.pi (λ (i : ι), ↑(f i)), cont := _}
@[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) :
↑(continuous_linear_map.pi f) = linear_map.pi (λ (i : ι), ↑(f 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 : ι) :
⇑(continuous_linear_map.pi f) c i = ⇑(f i) c
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) :
(continuous_linear_map.pi f).comp g = 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 : ι), module R (φ i)]
(i : ι) :
The projections from a family of topological modules are continuous linear maps.
Equations
- continuous_linear_map.proj i = {to_linear_map := linear_map.proj i, cont := _}
@[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) :
⇑(continuous_linear_map.proj i) b = b 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 : ι) :
(continuous_linear_map.proj i).comp (continuous_linear_map.pi f) = f 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) :
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
- continuous_linear_map.infi_ker_proj_equiv R φ hd hu = {to_linear_equiv := linear_map.infi_ker_proj_equiv R φ hd hu, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_map.map_neg
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(x : M) :
@[simp]
theorem
continuous_linear_map.map_sub
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_map.sub_apply'
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
(x : M) :
theorem
continuous_linear_map.range_prod_eq
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
{f : M →L[R] M₂}
{g : M →L[R] M₃}
(h : f.ker ⊔ g.ker = ⊤) :
theorem
continuous_linear_map.ker_prod_ker_le_ker_coprod
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f : M →L[R] M₃)
(g : M₂ →L[R] M₃) :
theorem
continuous_linear_map.ker_coprod_of_disjoint_range
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f : M →L[R] M₃)
(g : M₂ →L[R] M₃)
(hd : disjoint f.range g.range) :
@[protected, instance]
def
continuous_linear_map.has_neg
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M₂] :
@[simp]
theorem
continuous_linear_map.neg_apply
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
(x : M)
[topological_add_group M₂] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_neg
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
[topological_add_group M₂] :
@[norm_cast]
theorem
continuous_linear_map.coe_neg'
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →L[R] M₂)
[topological_add_group M₂] :
@[protected, instance]
def
continuous_linear_map.has_sub
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M₂] :
theorem
continuous_linear_map.continuous_gsmul
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[topological_add_group M₂]
(n : ℤ) :
continuous (λ (x : M₂), n • x)
@[continuity]
theorem
continuous_linear_map.continuous.gsmul
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[topological_add_group M₂]
{α : Type u_1}
[topological_space α]
{n : ℤ}
{f : α → M₂}
(hf : continuous f) :
continuous (λ (x : α), n • f x)
@[protected, instance]
def
continuous_linear_map.add_comm_group
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M₂] :
add_comm_group (M →L[R] M₂)
Equations
- continuous_linear_map.add_comm_group = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (f : M →L[R] M₂), {to_linear_map := {to_fun := λ (x : M), n • ⇑f x, map_add' := _, map_smul' := _}, cont := _}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg continuous_linear_map.has_neg, sub := has_sub.sub continuous_linear_map.has_sub, sub_eq_add_neg := _, gsmul := λ (n : ℤ) (f : M →L[R] M₂), {to_linear_map := {to_fun := λ (x : M), n • ⇑f x, map_add' := _, map_smul' := _}, cont := _}, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}
theorem
continuous_linear_map.sub_apply
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
[topological_add_group M₂]
(x : M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sub
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
[topological_add_group M₂] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sub'
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f g : M →L[R] M₂)
[topological_add_group M₂] :
@[protected, instance]
def
continuous_linear_map.ring
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M] :
Equations
- continuous_linear_map.ring = {add := add_comm_group.add continuous_linear_map.add_comm_group, add_assoc := _, zero := add_comm_group.zero continuous_linear_map.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul continuous_linear_map.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg continuous_linear_map.add_comm_group, sub := add_comm_group.sub continuous_linear_map.add_comm_group, sub_eq_add_neg := _, gsmul := add_comm_group.gsmul continuous_linear_map.add_comm_group, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul continuous_linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul continuous_linear_map.ring._proof_15 continuous_linear_map.ring._proof_16, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
theorem
continuous_linear_map.smul_right_one_pow
{R : Type u_1}
[ring R]
[topological_space R]
[topological_ring R]
(c : R)
(n : ℕ) :
1.smul_right c ^ n = 1.smul_right (c ^ n)
def
continuous_linear_map.proj_ker_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁) :
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
- f₁.proj_ker_of_right_inverse f₂ h = (continuous_linear_map.id R M - f₂.comp f₁).cod_restrict f₁.ker _
@[simp]
theorem
continuous_linear_map.coe_proj_ker_of_right_inverse_apply
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
@[simp]
theorem
continuous_linear_map.proj_ker_of_right_inverse_apply_idem
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : ↥(f₁.ker)) :
⇑(f₁.proj_ker_of_right_inverse f₂ 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}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(y : M₂) :
⇑(f₁.proj_ker_of_right_inverse f₂ h) (⇑f₂ y) = 0
@[protected, instance]
def
continuous_linear_map.has_scalar
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group 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₃)
@[simp]
theorem
continuous_linear_map.smul_comp
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group 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₂) :
theorem
continuous_linear_map.smul_apply
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group 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₂] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_smul
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group 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₂] :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_smul'
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group 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₂] :
@[simp]
theorem
continuous_linear_map.comp_smul
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group 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] :
def
continuous_linear_map.prod_equiv
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group M₃]
[module R M₃] :
continuous_linear_map.prod as an equiv.
@[simp]
theorem
continuous_linear_map.prod_equiv_apply
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group M₃]
[module R 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}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group M₃]
[module R M₃]
{f g : M × M₂ →L[R] M₃} :
f = g ↔ f.comp (continuous_linear_map.inl R M M₂) = g.comp (continuous_linear_map.inl R M M₂) ∧ f.comp (continuous_linear_map.inr R M M₂) = g.comp (continuous_linear_map.inr R M M₂)
@[ext]
theorem
continuous_linear_map.prod_ext
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group 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
@[protected, instance]
def
continuous_linear_map.module
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[module S M₂]
[has_continuous_smul S M₂]
[smul_comm_class R S M₂]
[has_continuous_add M₂] :
Equations
- continuous_linear_map.module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := continuous_linear_map.has_scalar _inst_17, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
continuous_linear_map.prodₗ_apply
{R : Type u_1}
(S : Type u_2)
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group 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)
[ring R]
[ring S]
[topological_space S]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group 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₃] :
continuous_linear_map.prod as a linear_equiv.
Equations
- continuous_linear_map.prodₗ S = {to_fun := continuous_linear_map.prod_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.prod_equiv.inv_fun, left_inv := _, right_inv := _}
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) :
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
- c.smul_rightₗ = {to_fun := c.smul_right, map_add' := _, map_smul' := _}
@[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) :
⇑(c.smul_rightₗ) = c.smul_right
@[protected, 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₂] :
Equations
- continuous_linear_map.algebra = algebra.of_module continuous_linear_map.algebra._proof_3 continuous_linear_map.algebra._proof_4
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₂) :
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
- continuous_linear_map.restrict_scalars R f = {to_linear_map := linear_map.restrict_scalars R ↑f, cont := _}
@[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]
[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₂] :
continuous_linear_map.restrict_scalars as a linear_map. See also
continuous_linear_map.restrict_scalarsL.
Equations
- continuous_linear_map.restrict_scalarsₗ A M M₂ R S = {to_fun := continuous_linear_map.restrict_scalars R _inst_11, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_restrict_scalarsₗ
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
{S : Type u_5}
[ring S]
[topological_space S]
[module S M₂]
[has_continuous_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
[topological_add_group M₂] :
def
continuous_linear_equiv.to_continuous_linear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
A continuous linear equivalence induces a continuous linear map.
Equations
- e.to_continuous_linear_map = {to_linear_map := {to_fun := e.to_linear_equiv.to_linear_map.to_fun, map_add' := _, map_smul' := _}, cont := _}
@[protected, instance]
def
continuous_linear_equiv.continuous_linear_map.has_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Coerce continuous linear equivs to continuous linear maps.
@[protected, instance]
def
continuous_linear_equiv.has_coe_to_fun
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
has_coe_to_fun (M ≃L[R] M₂)
Coerce continuous linear equivs to maps.
@[simp]
theorem
continuous_linear_equiv.coe_def_rev
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
theorem
continuous_linear_equiv.coe_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(b : M) :
@[simp]
theorem
continuous_linear_equiv.coe_to_linear_equiv
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M ≃L[R] M₂) :
⇑(f.to_linear_equiv) = ⇑f
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
theorem
continuous_linear_equiv.to_linear_equiv_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
@[ext]
theorem
continuous_linear_equiv.ext
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f g : M ≃L[R] M₂}
(h : ⇑f = ⇑g) :
f = g
theorem
continuous_linear_equiv.coe_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_inj
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{e e' : M ≃L[R] M₂} :
def
continuous_linear_equiv.to_homeomorph
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
M ≃ₜ M₂
A continuous linear equivalence induces a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := e.to_linear_equiv.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_to_homeomorph
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
⇑(e.to_homeomorph) = ⇑e
theorem
continuous_linear_equiv.image_closure
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(s : set M) :
theorem
continuous_linear_equiv.preimage_closure
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(s : set M₂) :
@[simp]
theorem
continuous_linear_equiv.is_closed_image
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
{s : set M} :
theorem
continuous_linear_equiv.map_nhds_eq
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(x : M) :
@[simp]
theorem
continuous_linear_equiv.map_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.map_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_equiv.map_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(c : R)
(x : M) :
@[simp]
theorem
continuous_linear_equiv.map_eq_zero_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
{x : M} :
@[protected, continuity]
theorem
continuous_linear_equiv.continuous
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[protected]
theorem
continuous_linear_equiv.continuous_on
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
{s : set M} :
continuous_on ⇑e s
@[protected]
theorem
continuous_linear_equiv.continuous_at
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
{x : M} :
continuous_at ⇑e x
@[protected]
theorem
continuous_linear_equiv.continuous_within_at
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
{s : set M}
{x : M} :
continuous_within_at ⇑e s x
theorem
continuous_linear_equiv.comp_continuous_on_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{α : Type u_4}
[topological_space α]
(e : M ≃L[R] M₂)
{f : α → M}
{s : set α} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
theorem
continuous_linear_equiv.comp_continuous_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{α : Type u_4}
[topological_space α]
(e : M ≃L[R] M₂)
{f : α → M} :
continuous (⇑e ∘ f) ↔ continuous f
theorem
continuous_linear_equiv.ext₁
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
[topological_space R]
{f g : R ≃L[R] M}
(h : ⇑f 1 = ⇑g 1) :
f = g
An extensionality lemma for R ≃L[R] M.
@[protected]
def
continuous_linear_equiv.refl
(R : Type u_1)
[semiring R]
(M : Type u_2)
[topological_space M]
[add_comm_monoid M]
[module R M] :
The identity map as a continuous linear equivalence.
Equations
- continuous_linear_equiv.refl R M = {to_linear_equiv := {to_fun := (linear_equiv.refl R M).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.refl R M).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_refl
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_refl'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
⇑(continuous_linear_equiv.refl R M) = id
@[protected]
def
continuous_linear_equiv.symm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
The inverse of a continuous linear equivalence as a continuous linear equivalence
Equations
- e.symm = {to_linear_equiv := {to_fun := e.to_linear_equiv.symm.to_fun, map_add' := _, map_smul' := _, inv_fun := e.to_linear_equiv.symm.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.symm_to_linear_equiv
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_to_homeomorph
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
theorem
continuous_linear_equiv.symm_map_nhds_eq
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(x : M) :
@[protected]
def
continuous_linear_equiv.trans
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(e₁ : M ≃L[R] M₂)
(e₂ : M₂ ≃L[R] M₃) :
The composition of two continuous linear equivalences as a continuous linear equivalence.
Equations
- e₁.trans e₂ = {to_linear_equiv := {to_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.trans_to_linear_equiv
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(e₁ : M ≃L[R] M₂)
(e₂ : M₂ ≃L[R] M₃) :
(e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv
def
continuous_linear_equiv.prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄) :
Product of two continuous linear equivalences. The map comes from equiv.prod_congr.
Equations
- e.prod e' = {to_linear_equiv := {to_fun := (e.to_linear_equiv.prod e'.to_linear_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e.to_linear_equiv.prod e'.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp, norm_cast]
theorem
continuous_linear_equiv.prod_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(x : M × M₃) :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄) :
theorem
continuous_linear_equiv.bijective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
theorem
continuous_linear_equiv.injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
theorem
continuous_linear_equiv.surjective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.trans_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(e₁ : M ≃L[R] M₂)
(e₂ : M₂ ≃L[R] M₃)
(c : M) :
@[simp]
theorem
continuous_linear_equiv.apply_symm_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(c : M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_apply_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(b : M) :
@[simp]
theorem
continuous_linear_equiv.symm_trans_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(e₁ : M₂ ≃L[R] M)
(e₂ : M₃ ≃L[R] M₂)
(c : M) :
@[simp]
theorem
continuous_linear_equiv.symm_image_image
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(s : set M) :
@[simp]
theorem
continuous_linear_equiv.image_symm_image
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(s : set M₂) :
@[simp, norm_cast]
theorem
continuous_linear_equiv.comp_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M ≃L[R] M₂)
(f' : M₂ ≃L[R] M₃) :
@[simp]
theorem
continuous_linear_equiv.coe_comp_coe_symm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.coe_symm_comp_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_comp_self
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.self_comp_symm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_symm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂) :
@[simp]
theorem
continuous_linear_equiv.refl_symm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M] :
theorem
continuous_linear_equiv.symm_symm_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(e : M ≃L[R] M₂)
(x : M) :