# Documentation

Mathlib.Algebra.Support

# 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}.

def Function.support {α : Type u_1} {A : Type u_3} [Zero A] (f : αA) :
Set α

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

Instances For
def Function.mulSupport {α : Type u_1} {M : Type u_5} [One M] (f : αM) :
Set α

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

Instances For
theorem Function.support_eq_preimage {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) :
= f ⁻¹' {0}
theorem Function.mulSupport_eq_preimage {α : Type u_1} {M : Type u_5} [One M] (f : αM) :
= f ⁻¹' {1}
theorem Function.nmem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {x : α} :
¬ f x = 0
theorem Function.nmem_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : αM} {x : α} :
f x = 1
theorem Function.compl_support {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} :
= {x | f x = 0}
theorem Function.compl_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : αM} :
= {x | f x = 1}
@[simp]
theorem Function.mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {x : α} :
f x 0
@[simp]
theorem Function.mem_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : αM} {x : α} :
f x 1
@[simp]
theorem Function.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
∀ (x : α), f x 0x s
@[simp]
theorem Function.mulSupport_subset_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
∀ (x : α), f x 1x s
theorem Function.support_subset_iff' {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
∀ (x : α), ¬x sf x = 0
theorem Function.mulSupport_subset_iff' {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
∀ (x : α), ¬x sf x = 1
theorem Function.support_eq_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
(∀ (x : α), x sf x 0) ∀ (x : α), ¬x sf x = 0
theorem Function.mulSupport_eq_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
(∀ (x : α), x sf x 1) ∀ (x : α), ¬x sf x = 1
theorem Function.support_disjoint_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
Set.EqOn f 0 s
theorem Function.mulSupport_disjoint_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
Set.EqOn f 1 s
theorem Function.disjoint_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
Set.EqOn f 0 s
theorem Function.disjoint_mulSupport_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
Set.EqOn f 1 s
@[simp]
theorem Function.support_eq_empty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} :
f = 0
@[simp]
theorem Function.mulSupport_eq_empty_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} :
f = 1
@[simp]
theorem Function.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} :
f 0
@[simp]
theorem Function.mulSupport_nonempty_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} :
f 1
theorem Function.range_subset_insert_image_support {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) :
insert 0 ()
theorem Function.range_subset_insert_image_mulSupport {α : Type u_1} {M : Type u_5} [One M] (f : αM) :
insert 1 ()
@[simp]
theorem Function.support_zero' {α : Type u_1} {M : Type u_5} [Zero M] :
@[simp]
theorem Function.mulSupport_one' {α : Type u_1} {M : Type u_5} [One M] :
@[simp]
theorem Function.support_zero {α : Type u_1} {M : Type u_5} [Zero M] :
(Function.support fun x => 0) =
@[simp]
theorem Function.mulSupport_one {α : Type u_1} {M : Type u_5} [One M] :
theorem Function.support_const {α : Type u_1} {M : Type u_5} [Zero M] {c : M} (hc : c 0) :
(Function.support fun x => c) = Set.univ
theorem Function.mulSupport_const {α : Type u_1} {M : Type u_5} [One M] {c : M} (hc : c 1) :
(Function.mulSupport fun x => c) = Set.univ
theorem Function.support_binop_subset {α : Type u_1} {M : Type u_5} {N : Type u_6} {P : Type u_7} [Zero M] [Zero N] [Zero P] (op : MNP) (op1 : op 0 0 = 0) (f : αM) (g : αN) :
(Function.support fun x => op (f x) (g x))
theorem Function.mulSupport_binop_subset {α : Type u_1} {M : Type u_5} {N : Type u_6} {P : Type u_7} [One M] [One N] [One P] (op : MNP) (op1 : op 1 1 = 1) (f : αM) (g : αN) :
(Function.mulSupport fun x => op (f x) (g x))
theorem Function.support_sup {α : Type u_1} {M : Type u_5} [Zero M] [] (f : αM) (g : αM) :
(Function.support fun x => f x g x)
theorem Function.mulSupport_sup {α : Type u_1} {M : Type u_5} [One M] [] (f : αM) (g : αM) :
(Function.mulSupport fun x => f x g x)
theorem Function.support_inf {α : Type u_1} {M : Type u_5} [Zero M] [] (f : αM) (g : αM) :
(Function.support fun x => f x g x)
theorem Function.mulSupport_inf {α : Type u_1} {M : Type u_5} [One M] [] (f : αM) (g : αM) :
(Function.mulSupport fun x => f x g x)
theorem Function.support_max {α : Type u_1} {M : Type u_5} [Zero M] [] (f : αM) (g : αM) :
(Function.support fun x => max (f x) (g x))
theorem Function.mulSupport_max {α : Type u_1} {M : Type u_5} [One M] [] (f : αM) (g : αM) :
(Function.mulSupport fun x => max (f x) (g x))
theorem Function.support_min {α : Type u_1} {M : Type u_5} [Zero M] [] (f : αM) (g : αM) :
(Function.support fun x => min (f x) (g x))
theorem Function.mulSupport_min {α : Type u_1} {M : Type u_5} [One M] [] (f : αM) (g : αM) :
(Function.mulSupport fun x => min (f x) (g x))
theorem Function.support_iSup {α : Type u_1} {M : Type u_5} {ι : Sort u_13} [Zero M] [] (f : ιαM) :
(Function.support fun x => ⨆ (i : ι), f i x) ⋃ (i : ι), Function.support (f i)
theorem Function.mulSupport_iSup {α : Type u_1} {M : Type u_5} {ι : Sort u_13} [One M] [] (f : ιαM) :
(Function.mulSupport fun x => ⨆ (i : ι), f i x) ⋃ (i : ι), Function.mulSupport (f i)
theorem Function.support_iInf {α : Type u_1} {M : Type u_5} {ι : Sort u_13} [Zero M] [] (f : ιαM) :
(Function.support fun x => ⨅ (i : ι), f i x) ⋃ (i : ι), Function.support (f i)
theorem Function.mulSupport_iInf {α : Type u_1} {M : Type u_5} {ι : Sort u_13} [One M] [] (f : ιαM) :
(Function.mulSupport fun x => ⨅ (i : ι), f i x) ⋃ (i : ι), Function.mulSupport (f i)
theorem Function.support_comp_subset {α : Type u_1} {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] {g : MN} (hg : g 0 = 0) (f : αM) :
theorem Function.mulSupport_comp_subset {α : Type u_1} {M : Type u_5} {N : Type u_6} [One M] [One N] {g : MN} (hg : g 1 = 1) (f : αM) :
theorem Function.support_subset_comp {α : Type u_1} {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] {g : MN} (hg : ∀ {x : M}, g x = 0x = 0) (f : αM) :
theorem Function.mulSupport_subset_comp {α : Type u_1} {M : Type u_5} {N : Type u_6} [One M] [One N] {g : MN} (hg : ∀ {x : M}, g x = 1x = 1) (f : αM) :
theorem Function.support_comp_eq {α : Type u_1} {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] (g : MN) (hg : ∀ {x : M}, g x = 0 x = 0) (f : αM) :
theorem Function.mulSupport_comp_eq {α : Type u_1} {M : Type u_5} {N : Type u_6} [One M] [One N] (g : MN) (hg : ∀ {x : M}, g x = 1 x = 1) (f : αM) :
theorem Function.support_comp_eq_of_range_subset {α : Type u_1} {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] {g : MN} {f : αM} (hg : ∀ {x : M}, x → (g x = 0 x = 0)) :
theorem Function.mulSupport_comp_eq_of_range_subset {α : Type u_1} {M : Type u_5} {N : Type u_6} [One M] [One N] {g : MN} {f : αM} (hg : ∀ {x : M}, x → (g x = 1 x = 1)) :
theorem Function.support_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (g : βM) (f : αβ) :
theorem Function.mulSupport_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (g : βM) (f : αβ) :
theorem Function.support_prod_mk {α : Type u_1} {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] (f : αM) (g : αN) :
(Function.support fun x => (f x, g x)) =
theorem Function.mulSupport_prod_mk {α : Type u_1} {M : Type u_5} {N : Type u_6} [One M] [One N] (f : αM) (g : αN) :
(Function.mulSupport fun x => (f x, g x)) =
theorem Function.support_prod_mk' {α : Type u_1} {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] (f : αM × N) :
= (Function.support fun x => (f x).fst) Function.support fun x => (f x).snd
theorem Function.mulSupport_prod_mk' {α : Type u_1} {M : Type u_5} {N : Type u_6} [One M] [One N] (f : αM × N) :
= (Function.mulSupport fun x => (f x).fst) Function.mulSupport fun x => (f x).snd
theorem Function.support_along_fiber_subset {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × βM) (a : α) :
(Function.support fun b => f (a, b)) Prod.snd ''
theorem Function.mulSupport_along_fiber_subset {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × βM) (a : α) :
(Function.mulSupport fun b => f (a, b)) Prod.snd ''
@[simp]
theorem Function.support_along_fiber_finite_of_finite {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × βM) (a : α) (h : ) :
Set.Finite (Function.support fun b => f (a, b))
@[simp]
theorem Function.mulSupport_along_fiber_finite_of_finite {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × βM) (a : α) (h : ) :
Set.Finite (Function.mulSupport fun b => f (a, b))
theorem Function.support_add {α : Type u_1} {M : Type u_5} [] (f : αM) (g : αM) :
(Function.support fun x => f x + g x)
theorem Function.mulSupport_mul {α : Type u_1} {M : Type u_5} [] (f : αM) (g : αM) :
(Function.mulSupport fun x => f x * g x)
theorem Function.support_nsmul {α : Type u_1} {M : Type u_5} [] (f : αM) (n : ) :
(Function.support fun x => n f x)
theorem Function.mulSupport_pow {α : Type u_1} {M : Type u_5} [] (f : αM) (n : ) :
(Function.mulSupport fun x => f x ^ n)
@[simp]
theorem Function.support_neg {α : Type u_1} {G : Type u_10} (f : αG) :
(Function.support fun x => -f x) =
@[simp]
theorem Function.mulSupport_inv {α : Type u_1} {G : Type u_10} [] (f : αG) :
(Function.mulSupport fun x => (f x)⁻¹) =
@[simp]
theorem Function.support_neg' {α : Type u_1} {G : Type u_10} (f : αG) :
@[simp]
theorem Function.mulSupport_inv' {α : Type u_1} {G : Type u_10} [] (f : αG) :
theorem Function.support_add_neg {α : Type u_1} {G : Type u_10} (f : αG) (g : αG) :
(Function.support fun x => f x + -g x)
theorem Function.mulSupport_mul_inv {α : Type u_1} {G : Type u_10} [] (f : αG) (g : αG) :
(Function.mulSupport fun x => f x * (g x)⁻¹)
theorem Function.support_sub {α : Type u_1} {G : Type u_10} (f : αG) (g : αG) :
(Function.support fun x => f x - g x)
theorem Function.mulSupport_div {α : Type u_1} {G : Type u_10} [] (f : αG) (g : αG) :
(Function.mulSupport fun x => f x / g x)
@[simp]
theorem Function.support_one {α : Type u_1} (R : Type u_8) [Zero R] [One R] [] :
= Set.univ
@[simp]
theorem Function.mulSupport_zero {α : Type u_1} (R : Type u_8) [Zero R] [One R] [] :
= Set.univ
theorem Function.support_nat_cast {α : Type u_1} {R : Type u_8} [] [] {n : } (hn : n 0) :
= Set.univ
theorem Function.mulSupport_nat_cast {α : Type u_1} {R : Type u_8} [] [] {n : } (hn : n 1) :
= Set.univ
theorem Function.support_int_cast {α : Type u_1} {R : Type u_8} [] [] {n : } (hn : n 0) :
= Set.univ
theorem Function.mulSupport_int_cast {α : Type u_1} {R : Type u_8} [] [] {n : } (hn : n 1) :
= Set.univ
theorem Function.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_8} [Zero R] [Zero M] [] [] (f : αR) (g : αM) :
@[simp]
theorem Function.support_mul {α : Type u_1} {R : Type u_8} [] [] (f : αR) (g : αR) :
(Function.support fun x => f x * g x) =
theorem Function.support_mul_subset_left {α : Type u_1} {R : Type u_8} [] (f : αR) (g : αR) :
(Function.support fun x => f x * g x)
theorem Function.support_mul_subset_right {α : Type u_1} {R : Type u_8} [] (f : αR) (g : αR) :
(Function.support fun x => f x * g x)
theorem Function.support_smul_subset_right {α : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] (b : B) (f : αA) :
theorem Function.support_smul_subset_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] [Zero β] [] (f : αM) (g : αβ) :
theorem Function.support_const_smul_of_ne_zero {α : Type u_1} {M : Type u_5} {R : Type u_8} [] [] [Module R M] [] (c : R) (g : αM) (hc : c 0) :
@[simp]
theorem Function.support_inv {α : Type u_1} {G₀ : Type u_12} [] (f : αG₀) :
(Function.support fun x => (f x)⁻¹) =
@[simp]
theorem Function.support_div {α : Type u_1} {G₀ : Type u_12} [] (f : αG₀) (g : αG₀) :
(Function.support fun x => f x / g x) =
theorem Function.support_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (s : ) (f : αβM) :
(Function.support fun x => Finset.sum s fun i => f i x) ⋃ (i : α) (_ : i s), Function.support (f i)
theorem Function.mulSupport_prod {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (s : ) (f : αβM) :
(Function.mulSupport fun x => Finset.prod s fun i => f i x) ⋃ (i : α) (_ : i s), Function.mulSupport (f i)
theorem Function.support_prod_subset {α : Type u_1} {β : Type u_2} {A : Type u_3} (s : ) (f : αβA) :
(Function.support fun x => Finset.prod s fun i => f i x) ⋂ (i : α) (_ : i s), Function.support (f i)
theorem Function.support_prod {α : Type u_1} {β : Type u_2} {A : Type u_3} [] [] (s : ) (f : αβA) :
(Function.support fun x => Finset.prod s fun i => f i x) = ⋂ (i : α) (_ : i s), Function.support (f i)
theorem Function.mulSupport_one_add {α : Type u_1} {R : Type u_8} [One R] (f : αR) :
(Function.mulSupport fun x => 1 + f x) =
theorem Function.mulSupport_one_add' {α : Type u_1} {R : Type u_8} [One R] (f : αR) :
theorem Function.mulSupport_add_one {α : Type u_1} {R : Type u_8} [One R] (f : αR) :
(Function.mulSupport fun x => f x + 1) =
theorem Function.mulSupport_add_one' {α : Type u_1} {R : Type u_8} [One R] (f : αR) :
theorem Function.mulSupport_one_sub' {α : Type u_1} {R : Type u_8} [One R] [] (f : αR) :
theorem Function.mulSupport_one_sub {α : Type u_1} {R : Type u_8} [One R] [] (f : αR) :
(Function.mulSupport fun x => 1 - f x) =
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 = g '' (s Function.support (f g))
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 = g '' (s Function.mulSupport (f g))
theorem Pi.support_single_subset {A : Type u_1} {B : Type u_2} [] [Zero B] {a : A} {b : B} :
{a}
theorem Pi.mulSupport_mulSingle_subset {A : Type u_1} {B : Type u_2} [] [One B] {a : A} {b : B} :
{a}
theorem Pi.support_single_zero {A : Type u_1} {B : Type u_2} [] [Zero B] {a : A} :
theorem Pi.mulSupport_mulSingle_one {A : Type u_1} {B : Type u_2} [] [One B] {a : A} :
@[simp]
theorem Pi.support_single_of_ne {A : Type u_1} {B : Type u_2} [] [Zero B] {a : A} {b : B} (h : b 0) :
= {a}
@[simp]
theorem Pi.mulSupport_mulSingle_of_ne {A : Type u_1} {B : Type u_2} [] [One B] {a : A} {b : B} (h : b 1) :
= {a}
theorem Pi.support_single {A : Type u_1} {B : Type u_2} [] [Zero B] {a : A} {b : B} [] :
= if b = 0 then else {a}
theorem Pi.mulSupport_mulSingle {A : Type u_1} {B : Type u_2} [] [One B] {a : A} {b : B} [] :
= if b = 1 then else {a}
theorem Pi.support_single_disjoint {A : Type u_1} {B : Type u_2} [] [Zero B] {b : B} {b' : B} (hb : b 0) (hb' : b' 0) {i : A} {j : A} :
theorem Pi.mulSupport_mulSingle_disjoint {A : Type u_1} {B : Type u_2} [] [One B] {b : B} {b' : B} (hb : b 1) (hb' : b' 1) {i : A} {j : A} :
Disjoint () () i j