Support of a function #

In this file we define Function.support f = {x | f x ≠ 0} and prove its basic properties. We also define Function.mulSupport f = {x | f x ≠ 1}.

source

def Function.mulSupport {ι : Type u_1} {M : Type u_3} [One M] (f : ι → M) :

Set ι

mulSupport of a function is the set of points x such that f x ≠ 1.

Equations

Function.mulSupport f = {x : ι | f x ≠ 1}

Instances For

source

def Function.support {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) :

Set ι

support of a function is the set of points x such that f x ≠ 0.

Equations

Function.support f = {x : ι | f x ≠ 0}

Instances For

source

theorem Function.mulSupport_eq_preimage {ι : Type u_1} {M : Type u_3} [One M] (f : ι → M) :

mulSupport f = f ⁻¹' {1}ᶜ

source

theorem Function.support_eq_preimage {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) :

support f = f ⁻¹' {0}ᶜ

source

theorem Function.notMem_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {x : ι} :

¬x ∈ mulSupport f ↔ f x = 1

source

theorem Function.notMem_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {x : ι} :

¬x ∈ support f ↔ f x = 0

source

theorem Function.compl_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} :

(mulSupport f)ᶜ = {x : ι | f x = 1}

source

theorem Function.compl_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} :

(support f)ᶜ = {x : ι | f x = 0}

source

@[simp]

theorem Function.mem_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {x : ι} :

x ∈ mulSupport f ↔ f x ≠ 1

source

@[simp]

theorem Function.mem_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {x : ι} :

x ∈ support f ↔ f x ≠ 0

source

@[simp]

theorem Function.mulSupport_subset_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} :

mulSupport f ⊆ s ↔ ∀ (x : ι), f x ≠ 1 → x ∈ s

source

@[simp]

theorem Function.support_subset_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} :

support f ⊆ s ↔ ∀ (x : ι), f x ≠ 0 → x ∈ s

source

theorem Function.mulSupport_subset_iff' {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} :

mulSupport f ⊆ s ↔ ∀ (x : ι), ¬x ∈ s → f x = 1

source

theorem Function.support_subset_iff' {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} :

support f ⊆ s ↔ ∀ (x : ι), ¬x ∈ s → f x = 0

source

theorem Function.mulSupport_eq_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} :

mulSupport f = s ↔ (∀ (x : ι), x ∈ s → f x ≠ 1) ∧ ∀ (x : ι), ¬x ∈ s → f x = 1

source

theorem Function.support_eq_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} :

support f = s ↔ (∀ (x : ι), x ∈ s → f x ≠ 0) ∧ ∀ (x : ι), ¬x ∈ s → f x = 0

source

theorem Function.ext_iff_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f g : ι → M} :

f = g ↔ mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x

source

theorem Function.ext_iff_support {ι : Type u_1} {M : Type u_3} [Zero M] {f g : ι → M} :

f = g ↔ support f = support g ∧ ∀ (x : ι), x ∈ support f → f x = g x

source

theorem Function.mulSupport_update_of_ne_one {ι : Type u_1} {M : Type u_3} [One M] [DecidableEq ι] (f : ι → M) (x : ι) {y : M} (hy : y ≠ 1) :

mulSupport (update f x y) = insert x (mulSupport f)

source

theorem Function.support_update_of_ne_zero {ι : Type u_1} {M : Type u_3} [Zero M] [DecidableEq ι] (f : ι → M) (x : ι) {y : M} (hy : y ≠ 0) :

support (update f x y) = insert x (support f)

source

theorem Function.mulSupport_update_one {ι : Type u_1} {M : Type u_3} [One M] [DecidableEq ι] (f : ι → M) (x : ι) :

mulSupport (update f x 1) = mulSupport f \ {x}

source

theorem Function.support_update_zero {ι : Type u_1} {M : Type u_3} [Zero M] [DecidableEq ι] (f : ι → M) (x : ι) :

support (update f x 0) = support f \ {x}

source

theorem Function.mulSupport_update_eq_ite {ι : Type u_1} {M : Type u_3} [One M] [DecidableEq ι] [DecidableEq M] (f : ι → M) (x : ι) (y : M) :

mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

source

theorem Function.support_update_eq_ite {ι : Type u_1} {M : Type u_3} [Zero M] [DecidableEq ι] [DecidableEq M] (f : ι → M) (x : ι) (y : M) :

support (update f x y) = if y = 0 then support f \ {x} else insert x (support f)

source

theorem Function.mulSupport_extend_one_subset {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [One N] {f : ι → κ} {g : ι → N} :

mulSupport (extend f g 1) ⊆ f '' mulSupport g

source

theorem Function.support_extend_zero_subset {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [Zero N] {f : ι → κ} {g : ι → N} :

support (extend f g 0) ⊆ f '' support g

source

theorem Function.mulSupport_extend_one {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [One N] {f : ι → κ} {g : ι → N} (hf : Injective f) :

mulSupport (extend f g 1) = f '' mulSupport g

source

theorem Function.support_extend_zero {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [Zero N] {f : ι → κ} {g : ι → N} (hf : Injective f) :

support (extend f g 0) = f '' support g

source

theorem Function.mulSupport_disjoint_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} :

Disjoint (mulSupport f) s ↔ Set.EqOn f 1 s

source

theorem Function.support_disjoint_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} :

Disjoint (support f) s ↔ Set.EqOn f 0 s

source

theorem Function.disjoint_mulSupport_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} :

Disjoint s (mulSupport f) ↔ Set.EqOn f 1 s

source

theorem Function.disjoint_support_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} :

Disjoint s (support f) ↔ Set.EqOn f 0 s

source

@[simp]

theorem Function.mulSupport_eq_empty_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} :

mulSupport f = ∅ ↔ f = 1

source

@[simp]

theorem Function.support_eq_empty_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} :

support f = ∅ ↔ f = 0

source

@[simp]

theorem Function.mulSupport_nonempty_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} :

(mulSupport f).Nonempty ↔ f ≠ 1

source

@[simp]

theorem Function.support_nonempty_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} :

(support f).Nonempty ↔ f ≠ 0

source

theorem Subsingleton.mulSupport_eq {ι : Type u_1} {M : Type u_3} [One M] [Subsingleton M] (f : ι → M) :

Function.mulSupport f = ∅

source

theorem Subsingleton.support_eq {ι : Type u_1} {M : Type u_3} [Zero M] [Subsingleton M] (f : ι → M) :

Function.support f = ∅

source

theorem Function.range_subset_insert_image_mulSupport {ι : Type u_1} {M : Type u_3} [One M] (f : ι → M) :

Set.range f ⊆ insert 1 (f '' mulSupport f)

source

theorem Function.range_subset_insert_image_support {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) :

Set.range f ⊆ insert 0 (f '' support f)

source

theorem Function.range_eq_image_or_of_mulSupport_subset {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {k : Set ι} (h : mulSupport f ⊆ k) :

Set.range f = f '' k ∨ Set.range f = insert 1 (f '' k)

source

theorem Function.range_eq_image_or_of_support_subset {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {k : Set ι} (h : support f ⊆ k) :

Set.range f = f '' k ∨ Set.range f = insert 0 (f '' k)

source

@[simp]

theorem Function.mulSupport_one {ι : Type u_1} {M : Type u_3} [One M] :

mulSupport 1 = ∅

source

@[simp]

theorem Function.support_zero {ι : Type u_1} {M : Type u_3} [Zero M] :

support 0 = ∅

source

@[simp]

theorem Function.mulSupport_fun_one {ι : Type u_1} {M : Type u_3} [One M] :

(mulSupport fun (x : ι) => 1) = ∅

source

@[simp]

theorem Function.support_fun_zero {ι : Type u_1} {M : Type u_3} [Zero M] :

(support fun (x : ι) => 0) = ∅

source

@[deprecated Function.support_zero (since := "2025-07-31")]

theorem Function.support_zero' {ι : Type u_1} {M : Type u_3} [Zero M] :

support 0 = ∅

Alias of Function.support_zero.

source

@[deprecated Function.mulSupport_one (since := "2025-07-31")]

theorem Function.mulSupport_one' {ι : Type u_1} {M : Type u_3} [One M] :

mulSupport 1 = ∅

Alias of Function.mulSupport_one.

source

theorem Function.mulSupport_const {ι : Type u_1} {M : Type u_3} [One M] {c : M} (hc : c ≠ 1) :

(mulSupport fun (x : ι) => c) = Set.univ

source

theorem Function.support_const {ι : Type u_1} {M : Type u_3} [Zero M] {c : M} (hc : c ≠ 0) :

(support fun (x : ι) => c) = Set.univ

source

theorem Function.mulSupport_binop_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] (op : M → N → P) (op1 : op 1 1 = 1) (f : ι → M) (g : ι → N) :

(mulSupport fun (x : ι) => op (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g

source

theorem Function.support_binop_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] (op : M → N → P) (op1 : op 0 0 = 0) (f : ι → M) (g : ι → N) :

(support fun (x : ι) => op (f x) (g x)) ⊆ support f ∪ support g

source

theorem Function.mulSupport_comp_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {g : M → N} (hg : g 1 = 1) (f : ι → M) :

mulSupport (g ∘ f) ⊆ mulSupport f

source

theorem Function.support_comp_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {g : M → N} (hg : g 0 = 0) (f : ι → M) :

support (g ∘ f) ⊆ support f

source

theorem Function.mulSupport_subset_comp {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {g : M → N} (hg : ∀ {x : M}, g x = 1 → x = 1) (f : ι → M) :

mulSupport f ⊆ mulSupport (g ∘ f)

source

theorem Function.support_subset_comp {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {g : M → N} (hg : ∀ {x : M}, g x = 0 → x = 0) (f : ι → M) :

support f ⊆ support (g ∘ f)

source

theorem Function.mulSupport_comp_eq {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] (g : M → N) (hg : ∀ {x : M}, g x = 1 ↔ x = 1) (f : ι → M) :

mulSupport (g ∘ f) = mulSupport f

source

theorem Function.support_comp_eq {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (g : M → N) (hg : ∀ {x : M}, g x = 0 ↔ x = 0) (f : ι → M) :

support (g ∘ f) = support f

source

theorem Function.mulSupport_comp_eq_of_range_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {g : M → N} {f : ι → M} (hg : ∀ {x : M}, x ∈ Set.range f → (g x = 1 ↔ x = 1)) :

mulSupport (g ∘ f) = mulSupport f

source

theorem Function.support_comp_eq_of_range_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {g : M → N} {f : ι → M} (hg : ∀ {x : M}, x ∈ Set.range f → (g x = 0 ↔ x = 0)) :

support (g ∘ f) = support f

source

theorem Function.mulSupport_comp_eq_preimage {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (g : κ → M) (f : ι → κ) :

mulSupport (g ∘ f) = f ⁻¹' mulSupport g

source

theorem Function.support_comp_eq_preimage {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (g : κ → M) (f : ι → κ) :

support (g ∘ f) = f ⁻¹' support g

source

theorem Function.mulSupport_prodMk {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] (f : ι → M) (g : ι → N) :

(mulSupport fun (x : ι) => (f x, g x)) = mulSupport f ∪ mulSupport g

source

theorem Function.support_prodMk {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ι → M) (g : ι → N) :

(support fun (x : ι) => (f x, g x)) = support f ∪ support g

source

theorem Function.mulSupport_prodMk' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] (f : ι → M × N) :

mulSupport f = (mulSupport fun (x : ι) => (f x).1) ∪ mulSupport fun (x : ι) => (f x).2

source

theorem Function.support_prodMk' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ι → M × N) :

support f = (support fun (x : ι) => (f x).1) ∪ support fun (x : ι) => (f x).2

source

@[deprecated Function.support_prodMk (since := "2025-07-31")]

theorem Function.support_prod_mk {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ι → M) (g : ι → N) :

(support fun (x : ι) => (f x, g x)) = support f ∪ support g

Alias of Function.support_prodMk.

source

@[deprecated Function.mulSupport_prodMk (since := "2025-07-31")]

theorem Function.mulSupport_prod_mk {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] (f : ι → M) (g : ι → N) :

(mulSupport fun (x : ι) => (f x, g x)) = mulSupport f ∪ mulSupport g

Alias of Function.mulSupport_prodMk.

source

@[deprecated Function.support_prodMk' (since := "2025-07-31")]

theorem Function.support_prod_mk' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ι → M × N) :

support f = (support fun (x : ι) => (f x).1) ∪ support fun (x : ι) => (f x).2

Alias of Function.support_prodMk'.

source

@[deprecated Function.mulSupport_prodMk' (since := "2025-07-31")]

theorem Function.mulSupport_prod_mk' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] (f : ι → M × N) :

mulSupport f = (mulSupport fun (x : ι) => (f x).1) ∪ mulSupport fun (x : ι) => (f x).2

Alias of Function.mulSupport_prodMk'.

source

theorem Function.mulSupport_along_fiber_subset {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (f : ι × κ → M) (i : ι) :

(mulSupport fun (j : κ) => f (i, j)) ⊆ Prod.snd '' mulSupport f

source

theorem Function.support_along_fiber_subset {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (f : ι × κ → M) (i : ι) :

(support fun (j : κ) => f (i, j)) ⊆ Prod.snd '' support f

source

theorem Function.mulSupport_curry {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (f : ι × κ → M) :

mulSupport (curry f) = Prod.fst '' mulSupport f

source

theorem Function.support_curry {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (f : ι × κ → M) :

support (curry f) = Prod.fst '' support f

source

theorem Function.mulSupport_fun_curry {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (f : ι × κ → M) :

(mulSupport fun (i : ι) (j : κ) => f (i, j)) = Prod.fst '' mulSupport f

source

theorem Function.support_fun_curry {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (f : ι × κ → M) :

(support fun (i : ι) (j : κ) => f (i, j)) = Prod.fst '' support f

source

@[deprecated Function.support_fun_curry (since := "2025-07-31")]

theorem Function.support_curry' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (f : ι × κ → M) :

(support fun (i : ι) (j : κ) => f (i, j)) = Prod.fst '' support f

Alias of Function.support_fun_curry.

source

@[deprecated Function.mulSupport_fun_curry (since := "2025-07-31")]

theorem Function.mulSupport_curry' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (f : ι × κ → M) :

(mulSupport fun (i : ι) (j : κ) => f (i, j)) = Prod.fst '' mulSupport f

Alias of Function.mulSupport_fun_curry.

source

theorem Set.image_inter_mulSupport_eq {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] {f : ι → M} {s : Set κ} {g : κ → ι} :

g '' s ∩ Function.mulSupport f = g '' (s ∩ Function.mulSupport (f ∘ g))

source

theorem Set.image_inter_support_eq {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] {f : ι → M} {s : Set κ} {g : κ → ι} :

g '' s ∩ Function.support f = g '' (s ∩ Function.support (f ∘ g))

source

theorem Pi.mulSupport_mulSingle_subset {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} :

Function.mulSupport (mulSingle i a) ⊆ {i}

source

theorem Pi.support_single_subset {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} :

Function.support (single i a) ⊆ {i}

source

theorem Pi.mulSupport_mulSingle_one {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} :

Function.mulSupport (mulSingle i 1) = ∅

source

theorem Pi.support_single_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} :

Function.support (single i 0) = ∅

source

@[simp]

theorem Pi.mulSupport_mulSingle_of_ne {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} (h : a ≠ 1) :

Function.mulSupport (mulSingle i a) = {i}

source

@[simp]

theorem Pi.support_single_of_ne {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} (h : a ≠ 0) :

Function.support (single i a) = {i}

source

theorem Pi.mulSupport_mulSingle {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} [DecidableEq M] :

Function.mulSupport (mulSingle i a) = if a = 1 then ∅ else {i}

source

theorem Pi.support_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} [DecidableEq M] :

Function.support (single i a) = if a = 0 then ∅ else {i}

source

theorem Pi.subsingleton_mulSupport_mulSingle {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} :

(Function.mulSupport (mulSingle i a)).Subsingleton

source

theorem Pi.subsingleton_support_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} :

(Function.support (single i a)).Subsingleton

source

theorem Pi.mulSupport_mulSingle_disjoint {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i j : ι} {a b : M} (ha : a ≠ 1) (hb : b ≠ 1) :

Disjoint (Function.mulSupport (mulSingle i a)) (Function.mulSupport (mulSingle j b)) ↔ i ≠ j

source

theorem Pi.support_single_disjoint {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i j : ι} {a b : M} (ha : a ≠ 0) (hb : b ≠ 0) :

Disjoint (Function.support (single i a)) (Function.support (single j b)) ↔ i ≠ j

Documentation

Mathlib.Algebra.Notation.Support

Support of a function #