Documentation

Mathlib.Algebra.Notation.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.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
Instances For
    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
    Instances For
      theorem Function.mulSupport_eq_preimage {ι : Type u_1} {M : Type u_3} [One M] (f : ιM) :
      theorem Function.support_eq_preimage {ι : Type u_1} {M : Type u_3} [Zero M] (f : ιM) :
      theorem Function.notMem_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {x : ι} :
      xmulSupport f f x = 1
      theorem Function.notMem_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {x : ι} :
      xsupport f f x = 0
      @[deprecated Function.notMem_support (since := "2025-05-24")]
      theorem Function.nmem_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {x : ι} :
      xsupport f f x = 0

      Alias of Function.notMem_support.

      @[deprecated Function.notMem_mulSupport (since := "2025-05-24")]
      theorem Function.nmem_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {x : ι} :
      xmulSupport f f x = 1

      Alias of Function.notMem_mulSupport.

      theorem Function.compl_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} :
      (mulSupport f) = {x : ι | f x = 1}
      theorem Function.compl_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} :
      (support f) = {x : ι | f x = 0}
      @[simp]
      theorem Function.mem_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {x : ι} :
      x mulSupport f f x 1
      @[simp]
      theorem Function.mem_support {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {x : ι} :
      x support f f x 0
      @[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 1x s
      @[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 0x s
      theorem Function.mulSupport_subset_iff' {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {s : Set ι} :
      mulSupport f s xs, f x = 1
      theorem Function.support_subset_iff' {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {s : Set ι} :
      support f s xs, f x = 0
      theorem Function.mulSupport_eq_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {s : Set ι} :
      mulSupport f = s (∀ xs, f x 1) xs, f x = 1
      theorem Function.support_eq_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {s : Set ι} :
      support f = s (∀ xs, f x 0) xs, f x = 0
      theorem Function.ext_iff_mulSupport {ι : Type u_1} {M : Type u_3} [One M] {f g : ιM} :
      f = g mulSupport f = mulSupport g xmulSupport f, f x = g x
      theorem Function.ext_iff_support {ι : Type u_1} {M : Type u_3} [Zero M] {f g : ιM} :
      f = g support f = support g xsupport f, f x = g x
      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) :
      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)
      theorem Function.mulSupport_update_one {ι : Type u_1} {M : Type u_3} [One M] [DecidableEq ι] (f : ιM) (x : ι) :
      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}
      theorem Function.mulSupport_update_eq_ite {ι : Type u_1} {M : Type u_3} [One M] [DecidableEq ι] [DecidableEq M] (f : ιM) (x : ι) (y : M) :
      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)
      theorem Function.mulSupport_extend_one_subset {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [One N] {f : ικ} {g : ιN} :
      theorem Function.support_extend_zero_subset {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [Zero N] {f : ικ} {g : ιN} :
      theorem Function.mulSupport_extend_one {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [One N] {f : ικ} {g : ιN} (hf : Injective f) :
      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
      theorem Function.mulSupport_disjoint_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {s : Set ι} :
      theorem Function.support_disjoint_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {s : Set ι} :
      theorem Function.disjoint_mulSupport_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} {s : Set ι} :
      theorem Function.disjoint_support_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} {s : Set ι} :
      @[simp]
      theorem Function.mulSupport_eq_empty_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} :
      @[simp]
      theorem Function.support_eq_empty_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} :
      support f = f = 0
      @[simp]
      theorem Function.mulSupport_nonempty_iff {ι : Type u_1} {M : Type u_3} [One M] {f : ιM} :
      @[simp]
      theorem Function.support_nonempty_iff {ι : Type u_1} {M : Type u_3} [Zero M] {f : ιM} :
      theorem Function.range_subset_insert_image_mulSupport {ι : Type u_1} {M : Type u_3} [One M] (f : ιM) :
      theorem Function.range_subset_insert_image_support {ι : Type u_1} {M : Type u_3} [Zero M] (f : ιM) :
      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)
      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)
      @[simp]
      theorem Function.mulSupport_one {ι : Type u_1} {M : Type u_3} [One M] :
      @[simp]
      theorem Function.support_zero {ι : Type u_1} {M : Type u_3} [Zero M] :
      @[simp]
      theorem Function.mulSupport_fun_one {ι : Type u_1} {M : Type u_3} [One M] :
      (mulSupport fun (x : ι) => 1) =
      @[simp]
      theorem Function.support_fun_zero {ι : Type u_1} {M : Type u_3} [Zero M] :
      (support fun (x : ι) => 0) =
      @[deprecated Function.support_zero (since := "2025-07-31")]
      theorem Function.support_zero' {ι : Type u_1} {M : Type u_3} [Zero M] :

      Alias of Function.support_zero.

      @[deprecated Function.mulSupport_one (since := "2025-07-31")]
      theorem Function.mulSupport_one' {ι : Type u_1} {M : Type u_3} [One M] :

      Alias of Function.mulSupport_one.

      theorem Function.mulSupport_const {ι : Type u_1} {M : Type u_3} [One M] {c : M} (hc : c 1) :
      (mulSupport fun (x : ι) => c) = Set.univ
      theorem Function.support_const {ι : Type u_1} {M : Type u_3} [Zero M] {c : M} (hc : c 0) :
      (support fun (x : ι) => c) = Set.univ
      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 : MNP) (op1 : op 1 1 = 1) (f : ιM) (g : ιN) :
      (mulSupport fun (x : ι) => op (f x) (g x)) mulSupport f mulSupport g
      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 : MNP) (op1 : op 0 0 = 0) (f : ιM) (g : ιN) :
      (support fun (x : ι) => op (f x) (g x)) support f support g
      theorem Function.mulSupport_comp_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {g : MN} (hg : g 1 = 1) (f : ιM) :
      theorem Function.support_comp_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {g : MN} (hg : g 0 = 0) (f : ιM) :
      theorem Function.mulSupport_subset_comp {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {g : MN} (hg : ∀ {x : M}, g x = 1x = 1) (f : ιM) :
      theorem Function.support_subset_comp {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {g : MN} (hg : ∀ {x : M}, g x = 0x = 0) (f : ιM) :
      theorem Function.mulSupport_comp_eq {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] (g : MN) (hg : ∀ {x : M}, g x = 1 x = 1) (f : ιM) :
      theorem Function.support_comp_eq {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (g : MN) (hg : ∀ {x : M}, g x = 0 x = 0) (f : ιM) :
      theorem Function.mulSupport_comp_eq_of_range_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [One M] [One N] {g : MN} {f : ιM} (hg : ∀ {x : M}, x Set.range f → (g x = 1 x = 1)) :
      theorem Function.support_comp_eq_of_range_subset {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {g : MN} {f : ιM} (hg : ∀ {x : M}, x Set.range f → (g x = 0 x = 0)) :
      theorem Function.mulSupport_comp_eq_preimage {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (g : κM) (f : ικ) :
      theorem Function.support_comp_eq_preimage {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (g : κM) (f : ικ) :
      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
      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
      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
      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
      @[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.

      @[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.

      @[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'.

      @[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'.

      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
      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
      theorem Function.mulSupport_curry {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] (f : ι × κM) :
      theorem Function.support_curry {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] (f : ι × κM) :
      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
      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
      @[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.

      @[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.

      theorem Set.image_inter_mulSupport_eq {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [One M] {f : ιM} {s : Set κ} {g : κι} :
      theorem Set.image_inter_support_eq {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Zero M] {f : ιM} {s : Set κ} {g : κι} :
      theorem Pi.mulSupport_mulSingle_subset {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} :
      theorem Pi.support_single_subset {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} :
      theorem Pi.mulSupport_mulSingle_one {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} :
      theorem Pi.support_single_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} :
      @[simp]
      theorem Pi.mulSupport_mulSingle_of_ne {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} (h : a 1) :
      @[simp]
      theorem Pi.support_single_of_ne {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} (h : a 0) :
      theorem Pi.mulSupport_mulSingle {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i : ι} {a : M} [DecidableEq M] :
      theorem Pi.support_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i : ι} {a : M} [DecidableEq M] :
      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) :
      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) :