Commit 2022-08-17 12:46 22dce611

View on Github →

feat(linear_algebra/linear_pmap): introduce notation (#15751) We add the notation E →ₗ.[R] F for linear_pmap R E F inspired by the notation for pfun and linear_map.

Estimated changes

Modified src/analysis/convex/cone.lean

modified theorem exists_extension_of_le_sublinear

modified theorem riesz_extension.exists_top

modified theorem riesz_extension

Modified src/analysis/normed_space/hahn_banach/separation.lean

Modified src/linear_algebra/linear_pmap.lean

modified def linear_map.comp_pmap

modified theorem linear_map.comp_pmap_apply

modified def linear_map.to_pmap

modified def linear_pmap.cod_restrict

modified theorem linear_pmap.coe_smul

modified def linear_pmap.comp

modified def linear_pmap.coprod

modified theorem linear_pmap.coprod_apply

modified theorem linear_pmap.domain_sup

modified theorem linear_pmap.domain_sup_span_singleton

modified def linear_pmap.eq_locus

modified theorem linear_pmap.eq_of_eq_graph

modified theorem linear_pmap.eq_of_le_of_domain_eq

modified theorem linear_pmap.ext

modified theorem linear_pmap.ext_iff

modified def linear_pmap.graph

modified theorem linear_pmap.graph_fst_eq_zero_snd

modified theorem linear_pmap.image_iff

modified theorem linear_pmap.le_of_eq_locus_ge

modified theorem linear_pmap.le_of_le_graph

modified theorem linear_pmap.map_add

modified theorem linear_pmap.map_neg

modified theorem linear_pmap.map_smul

modified theorem linear_pmap.map_sub

modified theorem linear_pmap.map_zero

modified theorem linear_pmap.mem_domain_iff

modified theorem linear_pmap.mem_domain_iff_of_eq_graph

modified theorem linear_pmap.mem_graph

modified theorem linear_pmap.mem_graph_iff'

modified theorem linear_pmap.mem_graph_iff

modified theorem linear_pmap.mem_graph_snd_inj'

modified theorem linear_pmap.mem_graph_snd_inj

modified theorem linear_pmap.mem_range_iff

modified theorem linear_pmap.neg_apply

modified theorem linear_pmap.neg_graph

modified theorem linear_pmap.smul_apply

modified theorem linear_pmap.smul_graph

modified theorem linear_pmap.sup_apply

modified theorem linear_pmap.sup_h_of_disjoint

modified theorem linear_pmap.sup_span_singleton_apply_mk

modified theorem linear_pmap.to_fun_eq_coe