# Finitely supported functions and spans #

## Tags #

function with finite support, module, linear algebra

source
@[simp]
theorem Finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) :
LinearMap.ker (lsingle a) = ⊥
source
theorem Finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) (h : Disjoint s t) :
⨆ a ∈ s, LinearMap.range (lsingle a) ≤ ⨅ a ∈ t, LinearMap.ker (lapply a)
source
theorem Finsupp.iInf_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
⨅ (a : α), LinearMap.ker (lapply a) ≤ ⊥
source
theorem Finsupp.iSup_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
⨆ (a : α), LinearMap.range (lsingle a) = ⊤
source
theorem Finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) (hs : Disjoint s t) :
Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨆ a ∈ t, LinearMap.range (lsingle a))
source
theorem Finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (a : α) :
Submodule.span R (single a '' s) = Submodule.map (lsingle a) (Submodule.span R s)
source
theorem Finsupp.range_lmapDomain {α : Type u_1} {R : Type u_5} [Semiring R] {β : Type u_7} (u : α → β) :
LinearMap.range (lmapDomain R R u) = Submodule.span R (Set.range fun (x : α) => single (u x) 1)
source
theorem Submodule.exists_finset_of_mem_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (p : ι → Submodule R M) {m : M} (hm : m ∈ ⨆ (i : ι), p i) :
∃ (s : Finset ι), m ∈ ⨆ i ∈ s, p i
source
theorem Submodule.mem_iSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {p : ι → Submodule R M} {m : M} :
m ∈ ⨆ (i : ι), p i ↔ ∃ (s : Finset ι), m ∈ ⨆ i ∈ s, p i

`Submodule.exists_finset_of_mem_iSup` as an `iff`

source
theorem Submodule.mem_sSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {m : M} :
m ∈ sSup S ↔ ∃ (s : Finset (Submodule R M)), ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i