Documentation

Mathlib.Algebra.Group.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_5} [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_5} [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_5} [One M] (f : αM) :
          theorem Function.support_eq_preimage {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) :
          theorem Function.notMem_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : αM} {x : α} :
          xmulSupport f f x = 1
          theorem Function.notMem_support {α : Type u_1} {M : Type u_5} [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_5} [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_5} [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_5} [One M] {f : αM} :
          (mulSupport f) = {x : α | f x = 1}
          theorem Function.compl_support {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} :
          (support f) = {x : α | f x = 0}
          @[simp]
          theorem Function.mem_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : αM} {x : α} :
          x mulSupport f f x 1
          @[simp]
          theorem Function.mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {x : α} :
          x support f f x 0
          @[simp]
          theorem Function.mulSupport_subset_iff {α : Type u_1} {M : Type u_5} [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_5} [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_5} [One M] {f : αM} {s : Set α} :
          mulSupport f s xs, f x = 1
          theorem Function.support_subset_iff' {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
          support f s xs, f x = 0
          theorem Function.mulSupport_eq_iff {α : Type u_1} {M : Type u_5} [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_5} [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_5} [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_5} [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_5} [One M] [DecidableEq α] (f : αM) (x : α) {y : M} (hy : y 1) :
          theorem Function.support_update_of_ne_zero {α : Type u_1} {M : Type u_5} [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_5} [One M] [DecidableEq α] (f : αM) (x : α) :
          theorem Function.support_update_zero {α : Type u_1} {M : Type u_5} [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_5} [One M] [DecidableEq α] [DecidableEq M] (f : αM) (x : α) (y : M) :
          theorem Function.support_update_eq_ite {α : Type u_1} {M : Type u_5} [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} {M' : Type u_6} {N : Type u_7} [One N] {f : αM'} {g : αN} :
          theorem Function.support_extend_zero_subset {α : Type u_1} {M' : Type u_6} {N : Type u_7} [Zero N] {f : αM'} {g : αN} :
          theorem Function.mulSupport_extend_one {α : Type u_1} {M' : Type u_6} {N : Type u_7} [One N] {f : αM'} {g : αN} (hf : Injective f) :
          theorem Function.support_extend_zero {α : Type u_1} {M' : Type u_6} {N : Type u_7} [Zero N] {f : αM'} {g : αN} (hf : Injective f) :
          support (extend f g 0) = f '' support g
          theorem Function.mulSupport_disjoint_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
          theorem Function.support_disjoint_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
          theorem Function.disjoint_mulSupport_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} {s : Set α} :
          theorem Function.disjoint_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {s : Set α} :
          @[simp]
          theorem Function.mulSupport_eq_empty_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} :
          @[simp]
          theorem Function.support_eq_empty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} :
          support f = f = 0
          @[simp]
          theorem Function.mulSupport_nonempty_iff {α : Type u_1} {M : Type u_5} [One M] {f : αM} :
          @[simp]
          theorem Function.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} :
          theorem Function.range_subset_insert_image_mulSupport {α : Type u_1} {M : Type u_5} [One M] (f : αM) :
          theorem Function.range_subset_insert_image_support {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) :
          theorem Function.range_eq_image_or_of_mulSupport_subset {α : Type u_1} {M : Type u_5} [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_5} [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_5} [One M] :
          @[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] :
          (mulSupport fun (x : α) => 1) =
          @[simp]
          theorem Function.support_zero {α : Type u_1} {M : Type u_5} [Zero M] :
          (support fun (x : α) => 0) =
          theorem Function.mulSupport_const {α : Type u_1} {M : Type u_5} [One M] {c : M} (hc : c 1) :
          (mulSupport fun (x : α) => c) = Set.univ
          theorem Function.support_const {α : Type u_1} {M : Type u_5} [Zero M] {c : M} (hc : c 0) :
          (support fun (x : α) => c) = Set.univ
          theorem Function.mulSupport_binop_subset {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [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_5} {N : Type u_7} {P : Type u_8} [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_5} {N : Type u_7} [One M] [One N] {g : MN} (hg : g 1 = 1) (f : αM) :
          theorem Function.support_comp_subset {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {g : MN} (hg : g 0 = 0) (f : αM) :
          theorem Function.mulSupport_subset_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} [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_5} {N : Type u_7} [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_5} {N : Type u_7} [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_5} {N : Type u_7} [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_5} {N : Type u_7} [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_5} {N : Type u_7} [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_5} [One M] (g : βM) (f : αβ) :
          theorem Function.support_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (g : βM) (f : αβ) :
          theorem Function.mulSupport_prod_mk {α : Type u_1} {M : Type u_5} {N : Type u_7} [One M] [One N] (f : αM) (g : αN) :
          (mulSupport fun (x : α) => (f x, g x)) = mulSupport f mulSupport g
          theorem Function.support_prod_mk {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : αM) (g : αN) :
          (support fun (x : α) => (f x, g x)) = support f support g
          theorem Function.mulSupport_prod_mk' {α : Type u_1} {M : Type u_5} {N : Type u_7} [One M] [One N] (f : αM × N) :
          mulSupport f = (mulSupport fun (x : α) => (f x).1) mulSupport fun (x : α) => (f x).2
          theorem Function.support_prod_mk' {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : αM × N) :
          support f = (support fun (x : α) => (f x).1) support fun (x : α) => (f x).2
          theorem Function.mulSupport_along_fiber_subset {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × βM) (a : α) :
          (mulSupport fun (b : β) => f (a, b)) Prod.snd '' mulSupport f
          theorem Function.support_along_fiber_subset {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × βM) (a : α) :
          (support fun (b : β) => f (a, b)) Prod.snd '' support f
          theorem Function.mulSupport_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × βM) :
          theorem Function.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × βM) :
          theorem Function.mulSupport_curry' {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × βM) :
          (mulSupport fun (a : α) (b : β) => f (a, b)) = Prod.fst '' mulSupport f
          theorem Function.support_curry' {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × βM) :
          (support fun (a : α) (b : β) => f (a, b)) = Prod.fst '' support f
          theorem Function.mulSupport_mul {α : Type u_1} {M : Type u_5} [MulOneClass M] (f g : αM) :
          (mulSupport fun (x : α) => f x * g x) mulSupport f mulSupport g
          theorem Function.support_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f g : αM) :
          (support fun (x : α) => f x + g x) support f support g
          theorem Function.mulSupport_pow {α : Type u_1} {M : Type u_5} [Monoid M] (f : αM) (n : ) :
          (mulSupport fun (x : α) => f x ^ n) mulSupport f
          theorem Function.support_nsmul {α : Type u_1} {M : Type u_5} [AddMonoid M] (f : αM) (n : ) :
          (support fun (x : α) => n f x) support f
          @[simp]
          theorem Function.mulSupport_inv {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f : αG) :
          (mulSupport fun (x : α) => (f x)⁻¹) = mulSupport f
          @[simp]
          theorem Function.support_neg {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f : αG) :
          (support fun (x : α) => -f x) = support f
          @[simp]
          theorem Function.mulSupport_inv' {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f : αG) :
          @[simp]
          theorem Function.support_neg' {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f : αG) :
          theorem Function.mulSupport_mul_inv {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f g : αG) :
          (mulSupport fun (x : α) => f x * (g x)⁻¹) mulSupport f mulSupport g
          theorem Function.support_add_neg {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f g : αG) :
          (support fun (x : α) => f x + -g x) support f support g
          theorem Function.mulSupport_div {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f g : αG) :
          (mulSupport fun (x : α) => f x / g x) mulSupport f mulSupport g
          theorem Function.support_sub {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f g : αG) :
          (support fun (x : α) => f x - g x) support f support g
          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 {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} {b : B} :
          theorem Pi.support_single_subset {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} {b : B} :
          theorem Pi.mulSupport_mulSingle_one {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} :
          theorem Pi.support_single_zero {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} :
          @[simp]
          theorem Pi.mulSupport_mulSingle_of_ne {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} {b : B} (h : b 1) :
          @[simp]
          theorem Pi.support_single_of_ne {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} {b : B} (h : b 0) :
          theorem Pi.mulSupport_mulSingle {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} {b : B} [DecidableEq B] :
          theorem Pi.support_single {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} {b : B} [DecidableEq B] :
          theorem Pi.mulSupport_mulSingle_disjoint {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {b b' : B} (hb : b 1) (hb' : b' 1) {i j : A} :
          theorem Pi.support_single_disjoint {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {b b' : B} (hb : b 0) (hb' : b' 0) {i j : A} :