mathlib documentation

analysis.normed_space.conformal_linear_map

Conformal Linear Maps #

A continuous linear map between R-normed spaces X and Y is_conformal_map if it is a nonzero multiple of a linear isometry.

Main definitions #

Main results #

See analysis.normed_space.conformal_linear_map.inner_product for

Tags #

conformal

Warning #

The definition of conformality in this file does NOT require the maps to be orientation-preserving.

def is_conformal_map {R : Type u_1} {X : Type u_2} {Y : Type u_3} [normed_field R] [semi_normed_group X] [semi_normed_group Y] [semi_normed_space R X] [semi_normed_space R Y] (f' : X →L[R] Y) :
Prop

A continuous linear map f' is said to be conformal if it's a nonzero multiple of a linear isometry.

Equations
theorem is_conformal_map_const_smul {R : Type u_1} {M : Type u_2} [normed_field R] [semi_normed_group M] [semi_normed_space R M] {c : R} (hc : c 0) :
theorem is_conformal_map_of_subsingleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [semi_normed_group M] [semi_normed_group N] [semi_normed_space R M] [semi_normed_space R N] [h : subsingleton M] (f' : M →L[R] N) :
theorem is_conformal_map.comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {G : Type u_4} [normed_field R] [semi_normed_group M] [semi_normed_group N] [semi_normed_group G] [semi_normed_space R M] [semi_normed_space R N] [semi_normed_space R G] {f' : M →L[R] N} {g' : N →L[R] G} (hg' : is_conformal_map g') (hf' : is_conformal_map f') :
theorem is_conformal_map.injective {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [semi_normed_group N] [semi_normed_space R N] [normed_group M'] [normed_space R M'] {f' : M' →L[R] N} (h : is_conformal_map f') :
theorem is_conformal_map.ne_zero {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [semi_normed_group N] [semi_normed_space R N] [normed_group M'] [normed_space R M'] [nontrivial M'] {f' : M' →L[R] N} (hf' : is_conformal_map f') :
f' 0