# mathlib3documentation

linear_algebra.linear_pmap

# Partially defined linear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A `linear_pmap R E F` or `E →ₗ.[R] F` is a linear map from a submodule of `E` to `F`. We define a `semilattice_inf` with `order_bot` instance on this this, and define three operations:

• `mk_span_singleton` defines a partial linear map defined on the span of a singleton.
• `sup` takes two partial linear maps `f`, `g` that agree on the intersection of their domains, and returns the unique partial linear map on `f.domain ⊔ g.domain` that extends both `f` and `g`.
• `Sup` takes a `directed_on (≤)` set of partial linear maps, and returns the unique partial linear map on the `Sup` of their domains that extends all these maps.

Moreover, we define

• `linear_pmap.graph` is the graph of the partial linear map viewed as a submodule of `E × F`.

Partially defined maps are currently used in `mathlib` to prove Hahn-Banach theorem and its variations. Namely, `linear_pmap.Sup` implies that every chain of `linear_pmap`s is bounded above. They are also the basis for the theory of unbounded operators.

structure linear_pmap (R : Type u) [ring R] (E : Type v) [ E] (F : Type w) [ F] :
Type (max v w)

A `linear_pmap R E F` or `E →ₗ.[R] F` is a linear map from a submodule of `E` to `F`.

Instances for `linear_pmap`
@[protected, instance]
def linear_pmap.has_coe_to_fun {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
has_coe_to_fun (E →ₗ.[R] F) (λ (f : E →ₗ.[R] F), (f.domain) F)
Equations
@[simp]
theorem linear_pmap.to_fun_eq_coe {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (x : (f.domain)) :
(f.to_fun) x = f x
@[ext]
theorem linear_pmap.ext {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (h : f.domain = g.domain) (h' : ⦃x : (f.domain)⦄ ⦃y : (g.domain)⦄, x = y f x = g y) :
f = g
@[simp]
theorem linear_pmap.map_zero {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) :
f 0 = 0
theorem linear_pmap.ext_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} :
f = g (domain_eq : f.domain = g.domain), ⦃x : (f.domain)⦄ ⦃y : (g.domain)⦄, x = y f x = g y
theorem linear_pmap.ext' {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {s : E} {f g : s →ₗ[R] F} (h : f = g) :
{domain := s, to_fun := f} = {domain := s, to_fun := g}
theorem linear_pmap.map_add {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (x y : (f.domain)) :
f (x + y) = f x + f y
theorem linear_pmap.map_neg {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (x : (f.domain)) :
f (-x) = -f x
theorem linear_pmap.map_sub {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (x y : (f.domain)) :
f (x - y) = f x - f y
theorem linear_pmap.map_smul {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (c : R) (x : (f.domain)) :
f (c x) = c f x
@[simp]
theorem linear_pmap.mk_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (p : E) (f : p →ₗ[R] F) (x : p) :
{domain := p, to_fun := f} x = f x
noncomputable def linear_pmap.mk_span_singleton' {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (x : E) (y : F) (H : (c : R), c x = 0 c y = 0) :

The unique `linear_pmap` on `R ∙ x` that sends `x` to `y`. This version works for modules over rings, and requires a proof of `∀ c, c • x = 0 → c • y = 0`.

Equations
@[simp]
theorem linear_pmap.domain_mk_span_singleton {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (x : E) (y : F) (H : (c : R), c x = 0 c y = 0) :
.domain = {x}
@[simp]
theorem linear_pmap.mk_span_singleton'_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (x : E) (y : F) (H : (c : R), c x = 0 c y = 0) (c : R) (h : c x .domain) :
c x, h⟩ = c y
@[simp]
theorem linear_pmap.mk_span_singleton'_apply_self {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (x : E) (y : F) (H : (c : R), c x = 0 c y = 0) (h : x .domain) :
x, h⟩ = y
@[reducible]
noncomputable def linear_pmap.mk_span_singleton {K : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (x : E) (y : F) (hx : x 0) :

The unique `linear_pmap` on `span R {x}` that sends a non-zero vector `x` to `y`. This version works for modules over division rings.

Equations
theorem linear_pmap.mk_span_singleton_apply (K : Type u_1) {E : Type u_2} {F : Type u_3} [ E] [ F] {x : E} (hx : x 0) (y : F) :
hx) x, _⟩ = y
@[protected]
def linear_pmap.fst {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (p : E) (p' : F) :
E × F →ₗ.[R] E

Projection to the first coordinate as a `linear_pmap`

Equations
@[simp]
theorem linear_pmap.fst_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (p : E) (p' : F) (x : (p.prod p')) :
p') x = x.fst
@[protected]
def linear_pmap.snd {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (p : E) (p' : F) :
E × F →ₗ.[R] F

Projection to the second coordinate as a `linear_pmap`

Equations
@[simp]
theorem linear_pmap.snd_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (p : E) (p' : F) (x : (p.prod p')) :
p') x = x.snd
@[protected, instance]
def linear_pmap.has_neg {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
@[simp]
theorem linear_pmap.neg_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (x : ((-f).domain)) :
(-f) x = -f x
@[protected, instance]
def linear_pmap.has_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
theorem linear_pmap.apply_comp_of_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {T S : E →ₗ.[R] F} (h : T S) (x : (T.domain)) :
T x = S ( x)
theorem linear_pmap.exists_of_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {T S : E →ₗ.[R] F} (h : T S) (x : (T.domain)) :
(y : (S.domain)), x = y T x = S y
theorem linear_pmap.eq_of_le_of_domain_eq {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (hle : f g) (heq : f.domain = g.domain) :
f = g
def linear_pmap.eq_locus {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f g : E →ₗ.[R] F) :
E

Given two partial linear maps `f`, `g`, the set of points `x` such that both `f` and `g` are defined at `x` and `f x = g x` form a submodule.

Equations
@[protected, instance]
def linear_pmap.has_inf {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
@[protected, instance]
def linear_pmap.has_bot {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
@[protected, instance]
def linear_pmap.inhabited {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
@[protected, instance]
def linear_pmap.semilattice_inf {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
@[protected, instance]
def linear_pmap.order_bot {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
theorem linear_pmap.le_of_eq_locus_ge {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (H : f.domain f.eq_locus g) :
f g
theorem linear_pmap.domain_mono {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
@[protected]
noncomputable def linear_pmap.sup {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f g : E →ₗ.[R] F) (h : (x : (f.domain)) (y : (g.domain)), x = y f x = g y) :

Given two partial linear maps that agree on the intersection of their domains, `f.sup g h` is the unique partial linear map on `f.domain ⊔ g.domain` that agrees with `f` and `g`.

Equations
@[simp]
theorem linear_pmap.domain_sup {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f g : E →ₗ.[R] F) (h : (x : (f.domain)) (y : (g.domain)), x = y f x = g y) :
(f.sup g h).domain = f.domain g.domain
theorem linear_pmap.sup_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (H : (x : (f.domain)) (y : (g.domain)), x = y f x = g y) (x : (f.domain)) (y : (g.domain)) (z : ((f.sup g H).domain)) (hz : x + y = z) :
(f.sup g H) z = f x + g y
@[protected]
theorem linear_pmap.left_le_sup {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f g : E →ₗ.[R] F) (h : (x : (f.domain)) (y : (g.domain)), x = y f x = g y) :
f f.sup g h
@[protected]
theorem linear_pmap.right_le_sup {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f g : E →ₗ.[R] F) (h : (x : (f.domain)) (y : (g.domain)), x = y f x = g y) :
g f.sup g h
@[protected]
theorem linear_pmap.sup_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g h : E →ₗ.[R] F} (H : (x : (f.domain)) (y : (g.domain)), x = y f x = g y) (fh : f h) (gh : g h) :
f.sup g H h
theorem linear_pmap.sup_h_of_disjoint {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f g : E →ₗ.[R] F) (h : g.domain) (x : (f.domain)) (y : (g.domain)) (hxy : x = y) :
f x = g y

Hypothesis for `linear_pmap.sup` holds, if `f.domain` is disjoint with `g.domain`.

@[protected, instance]
def linear_pmap.has_smul {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} [monoid M] [ F] [ F] :
(E →ₗ.[R] F)
Equations
@[simp]
theorem linear_pmap.smul_domain {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} [monoid M] [ F] [ F] (a : M) (f : E →ₗ.[R] F) :
(a f).domain = f.domain
theorem linear_pmap.smul_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} [monoid M] [ F] [ F] (a : M) (f : E →ₗ.[R] F) (x : ((a f).domain)) :
(a f) x = a f x
@[simp]
theorem linear_pmap.coe_smul {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} [monoid M] [ F] [ F] (a : M) (f : E →ₗ.[R] F) :
(a f) = a f
@[protected, instance]
def linear_pmap.smul_comm_class {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} {N : Type u_6} [monoid M] [ F] [ F] [monoid N] [ F] [ F] [ F] :
(E →ₗ.[R] F)
@[protected, instance]
def linear_pmap.is_scalar_tower {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} {N : Type u_6} [monoid M] [ F] [ F] [monoid N] [ F] [ F] [ N] [ F] :
(E →ₗ.[R] F)
@[protected, instance]
def linear_pmap.mul_action {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} [monoid M] [ F] [ F] :
(E →ₗ.[R] F)
Equations
@[protected, instance]
def linear_pmap.has_vadd {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
@[simp]
theorem linear_pmap.vadd_domain {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) :
theorem linear_pmap.vadd_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) (x : ((f +ᵥ g).domain)) :
(f +ᵥ g) x = f x + g x
@[simp]
theorem linear_pmap.coe_vadd {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) :
@[protected, instance]
def linear_pmap.add_action {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] :
Equations
noncomputable def linear_pmap.sup_span_singleton {E : Type u_2} {F : Type u_3} {K : Type u_5} [ E] [ F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x f.domain) :

Extend a `linear_pmap` to `f.domain ⊔ K ∙ x`.

Equations
@[simp]
theorem linear_pmap.domain_sup_span_singleton {E : Type u_2} {F : Type u_3} {K : Type u_5} [ E] [ F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x f.domain) :
y hx).domain = f.domain {x}
@[simp]
theorem linear_pmap.sup_span_singleton_apply_mk {E : Type u_2} {F : Type u_3} {K : Type u_5} [ E] [ F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x f.domain) (x' : E) (hx' : x' f.domain) (c : K) :
y hx) x' + c x, _⟩ = f x', hx'⟩ + c y
@[protected]
noncomputable def linear_pmap.Sup {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (c : set (E →ₗ.[R] F)) (hc : c) :

Glue a collection of partially defined linear maps to a linear map defined on `Sup` of these submodules.

Equations
• hc =
@[protected]
theorem linear_pmap.le_Sup {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {c : set (E →ₗ.[R] F)} (hc : c) {f : E →ₗ.[R] F} (hf : f c) :
f hc
@[protected]
theorem linear_pmap.Sup_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {c : set (E →ₗ.[R] F)} (hc : c) {g : E →ₗ.[R] F} (hg : (f : E →ₗ.[R] F), f c f g) :
hc g
@[protected]
theorem linear_pmap.Sup_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {c : set (E →ₗ.[R] F)} (hc : c) {l : E →ₗ.[R] F} (hl : l c) (x : (l.domain)) :
hc) x, _⟩ = l x
def linear_map.to_pmap {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ[R] F) (p : E) :

Restrict a linear map to a submodule, reinterpreting the result as a `linear_pmap`.

Equations
@[simp]
theorem linear_map.to_pmap_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ[R] F) (p : E) (x : p) :
(f.to_pmap p) x = f x
@[simp]
theorem linear_map.to_pmap_domain {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ[R] F) (p : E) :
(f.to_pmap p).domain = p
def linear_map.comp_pmap {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (g : F →ₗ[R] G) (f : E →ₗ.[R] F) :

Compose a linear map with a `linear_pmap`

Equations
@[simp]
theorem linear_map.comp_pmap_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (g : F →ₗ[R] G) (f : E →ₗ.[R] F) (x : ((g.comp_pmap f).domain)) :
(g.comp_pmap f) x = g (f x)
def linear_pmap.cod_restrict {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (p : F) (H : (x : (f.domain)), f x p) :

Restrict codomain of a `linear_pmap`

Equations
def linear_pmap.comp {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) (H : (x : (f.domain)), f x g.domain) :

Compose two `linear_pmap`s

Equations
def linear_pmap.coprod {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) :
E × F →ₗ.[R] G

`f.coprod g` is the partially defined linear map defined on `f.domain × g.domain`, and sending `p` to `f p.1 + g p.2`.

Equations
@[simp]
theorem linear_pmap.coprod_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) (x : ((f.coprod g).domain)) :
(f.coprod g) x = f x.fst, _⟩ + g x.snd, _⟩
def linear_pmap.dom_restrict {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (S : E) :

Restrict a partially defined linear map to a submodule of `E` contained in `f.domain`.

Equations
@[simp]
theorem linear_pmap.dom_restrict_domain {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) {S : E} :
theorem linear_pmap.dom_restrict_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E →ₗ.[R] F} {S : E} ⦃x : (S f.domain) ⦃y : (f.domain)⦄ (h : x = y) :
(f.dom_restrict S) x = f y
theorem linear_pmap.dom_restrict_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E →ₗ.[R] F} {S : E} :

### Graph #

def linear_pmap.graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) :
(E × F)

The graph of a `linear_pmap` viewed as a submodule on `E × F`.

Equations
theorem linear_pmap.mem_graph_iff' {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) {x : E × F} :
x f.graph (y : (f.domain)), (y, f y) = x
@[simp]
theorem linear_pmap.mem_graph_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) {x : E × F} :
x f.graph (y : (f.domain)), y = x.fst f y = x.snd
theorem linear_pmap.mem_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) (x : (f.domain)) :
(x, f x) f.graph

The tuple `(x, f x)` is contained in the graph of `f`.

theorem linear_pmap.smul_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {M : Type u_5} [monoid M] [ F] [ F] (f : E →ₗ.[R] F) (z : M) :
(z f).graph =

The graph of `z • f` as a pushforward.

theorem linear_pmap.neg_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) :

The graph of `-f` as a pushforward.

theorem linear_pmap.mem_graph_snd_inj {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) {x y : E} {x' y' : F} (hx : (x, x') f.graph) (hy : (y, y') f.graph) (hxy : x = y) :
x' = y'
theorem linear_pmap.mem_graph_snd_inj' {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) {x y : E × F} (hx : x f.graph) (hy : y f.graph) (hxy : x.fst = y.fst) :
x.snd = y.snd
theorem linear_pmap.graph_fst_eq_zero_snd {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →ₗ.[R] F) {x : E} {x' : F} (h : (x, x') f.graph) (hx : x = 0) :
x' = 0

The property that `f 0 = 0` in terms of the graph.

theorem linear_pmap.mem_domain_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E →ₗ.[R] F} {x : E} :
x f.domain (y : F), (x, y) f.graph
theorem linear_pmap.mem_domain_of_mem_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E →ₗ.[R] F} {x : E} {y : F} (h : (x, y) f.graph) :
theorem linear_pmap.image_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E →ₗ.[R] F} {x : E} {y : F} (hx : x f.domain) :
y = f x, hx⟩ (x, y) f.graph
theorem linear_pmap.mem_range_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E →ₗ.[R] F} {y : F} :
y (x : E), (x, y) f.graph
theorem linear_pmap.mem_domain_iff_of_eq_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (h : f.graph = g.graph) {x : E} :
theorem linear_pmap.le_of_le_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (h : f.graph g.graph) :
f g
theorem linear_pmap.le_graph_of_le {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (h : f g) :
theorem linear_pmap.le_graph_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} :
theorem linear_pmap.eq_of_eq_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {f g : E →ₗ.[R] F} (h : f.graph = g.graph) :
f = g
theorem submodule.exists_unique_from_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {g : (E × F)} (hg : {x : E × F}, x g x.fst = 0 x.snd = 0) {a : E} (ha : a submodule.map E F) g) :
∃! (b : F), (a, b) g
noncomputable def submodule.val_from_graph {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {g : (E × F)} (hg : (x : E × F), x g x.fst = 0 x.snd = 0) {a : E} (ha : a submodule.map E F) g) :
F

Auxiliary definition to unfold the existential quantifier.

Equations
theorem submodule.val_from_graph_mem {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {g : (E × F)} (hg : (x : E × F), x g x.fst = 0 x.snd = 0) {a : E} (ha : a submodule.map E F) g) :
(a, ha) g
noncomputable def submodule.to_linear_pmap {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (g : (E × F)) (hg : (x : E × F), x g x.fst = 0 x.snd = 0) :

Define a `linear_pmap` from its graph.

Equations
theorem submodule.mem_graph_to_linear_pmap {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (g : (E × F)) (hg : (x : E × F), x g x.fst = 0 x.snd = 0) (x : (submodule.map E F) g)) :
(x.val, (g.to_linear_pmap hg) x) g
@[simp]
theorem submodule.to_linear_pmap_graph_eq {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] (g : (E × F)) (hg : (x : E × F), x g x.fst = 0 x.snd = 0) :