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

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

Instances For

source

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

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

Instances For

source

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

Function.support f = f ⁻¹' {0}ᶜ

source

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

Function.mulSupport f = f ⁻¹' {1}ᶜ

source

theorem Function.nmem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} {x : α} :

x ∉ Function.support f ↔ f x = 0

source

theorem Function.nmem_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : α → M} {x : α} :

x ∉ Function.mulSupport f ↔ f x = 1

source

theorem Function.compl_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} :

(Function.support f)ᶜ = {x : α | f x = 0}

source

theorem Function.compl_mulSupport {α : Type u_1} {M : Type u_5} [One M] {f : α → M} :

(Function.mulSupport f)ᶜ = {x : α | f x = 1}

source

@[simp]

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

x ∈ Function.support f ↔ f x ≠ 0

source

@[simp]

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

x ∈ Function.mulSupport f ↔ f x ≠ 1

source

@[simp]

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

Function.support f ⊆ s ↔ ∀ (x : α), f x ≠ 0 → x ∈ s

source

@[simp]

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

Function.mulSupport f ⊆ s ↔ ∀ (x : α), f x ≠ 1 → x ∈ s

source

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

Function.support f ⊆ s ↔ ∀ x ∉ s, f x = 0

source

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

Function.mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1

source

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

Function.support f = s ↔ (∀ x ∈ s, f x ≠ 0) ∧ ∀ x ∉ s, f x = 0

source

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

Function.mulSupport f = s ↔ (∀ x ∈ s, f x ≠ 1) ∧ ∀ x ∉ s, f x = 1

source

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

f = g ↔ Function.support f = Function.support g ∧ ∀ x ∈ Function.support f, f x = g x

source

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

f = g ↔ Function.mulSupport f = Function.mulSupport g ∧ ∀ x ∈ Function.mulSupport f, f x = g x

source

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) :

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

source

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) :

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

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem Function.support_extend_zero_subset {α : Type u_1} {M' : Type u_6} {N : Type u_7} [Zero N] {f : α → M'} {g : α → N} :

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

source

theorem Function.mulSupport_extend_one_subset {α : Type u_1} {M' : Type u_6} {N : Type u_7} [One N] {f : α → M'} {g : α → N} :

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

source

theorem Function.support_extend_zero {α : Type u_1} {M' : Type u_6} {N : Type u_7} [Zero N] {f : α → M'} {g : α → N} (hf : Function.Injective f) :

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

source

theorem Function.mulSupport_extend_one {α : Type u_1} {M' : Type u_6} {N : Type u_7} [One N] {f : α → M'} {g : α → N} (hf : Function.Injective f) :

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

theorem Function.support_eq_empty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} :

Function.support f = ∅ ↔ f = 0

source

@[simp]

theorem Function.mulSupport_eq_empty_iff {α : Type u_1} {M : Type u_5} [One M] {f : α → M} :

Function.mulSupport f = ∅ ↔ f = 1

source

@[simp]

theorem Function.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} :

(Function.support f).Nonempty ↔ f ≠ 0

source

@[simp]

theorem Function.mulSupport_nonempty_iff {α : Type u_1} {M : Type u_5} [One M] {f : α → M} :

(Function.mulSupport f).Nonempty ↔ f ≠ 1

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

theorem Function.support_zero' {α : Type u_1} {M : Type u_5} [Zero M] :

Function.support 0 = ∅

source

@[simp]

theorem Function.mulSupport_one' {α : Type u_1} {M : Type u_5} [One M] :

Function.mulSupport 1 = ∅

source

@[simp]

theorem Function.support_zero {α : Type u_1} {M : Type u_5} [Zero M] :

(Function.support fun (x : α) => 0) = ∅

source

@[simp]

theorem Function.mulSupport_one {α : Type u_1} {M : Type u_5} [One M] :

(Function.mulSupport fun (x : α) => 1) = ∅

source

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

source

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

source

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 : M → N → P) (op1 : op 0 0 = 0) (f : α → M) (g : α → N) :

(Function.support fun (x : α) => op (f x) (g x)) ⊆ Function.support f ∪ Function.support g

source

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 : M → N → P) (op1 : op 1 1 = 1) (f : α → M) (g : α → N) :

(Function.mulSupport fun (x : α) => op (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g

source

theorem Function.support_comp_subset {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {g : M → N} (hg : g 0 = 0) (f : α → M) :

Function.support (g ∘ f) ⊆ Function.support f

source

theorem Function.mulSupport_comp_subset {α : Type u_1} {M : Type u_5} {N : Type u_7} [One M] [One N] {g : M → N} (hg : g 1 = 1) (f : α → M) :

Function.mulSupport (g ∘ f) ⊆ Function.mulSupport f

source

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

Function.support f ⊆ Function.support (g ∘ f)

source

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

Function.mulSupport f ⊆ Function.mulSupport (g ∘ f)

source

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

Function.support (g ∘ f) = Function.support f

source

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

Function.mulSupport (g ∘ f) = Function.mulSupport f

source

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

Function.support (g ∘ f) = Function.support f

source

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

Function.mulSupport (g ∘ f) = Function.mulSupport f

source

theorem Function.support_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (g : β → M) (f : α → β) :

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

source

theorem Function.mulSupport_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (g : β → M) (f : α → β) :

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

source

theorem Function.support_prod_mk {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : α → M) (g : α → N) :

(Function.support fun (x : α) => (f x, g x)) = Function.support f ∪ Function.support g

source

theorem Function.mulSupport_prod_mk {α : Type u_1} {M : Type u_5} {N : Type u_7} [One M] [One N] (f : α → M) (g : α → N) :

(Function.mulSupport fun (x : α) => (f x, g x)) = Function.mulSupport f ∪ Function.mulSupport g

source

theorem Function.support_prod_mk' {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : α → M × N) :

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

source

theorem Function.mulSupport_prod_mk' {α : Type u_1} {M : Type u_5} {N : Type u_7} [One M] [One N] (f : α → M × N) :

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

source

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 '' Function.support f

source

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 '' Function.mulSupport f

source

theorem Function.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × β → M) :

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

source

theorem Function.mulSupport_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × β → M) :

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

source

theorem Function.support_curry' {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × β → M) :

(Function.support fun (a : α) (b : β) => f (a, b)) = Prod.fst '' Function.support f

source

theorem Function.mulSupport_curry' {α : Type u_1} {β : Type u_2} {M : Type u_5} [One M] (f : α × β → M) :

(Function.mulSupport fun (a : α) (b : β) => f (a, b)) = Prod.fst '' Function.mulSupport f

source

theorem Function.support_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α → M) (g : α → M) :

(Function.support fun (x : α) => f x + g x) ⊆ Function.support f ∪ Function.support g

source

theorem Function.mulSupport_mul {α : Type u_1} {M : Type u_5} [MulOneClass M] (f : α → M) (g : α → M) :

(Function.mulSupport fun (x : α) => f x * g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g

source

theorem Function.support_nsmul {α : Type u_1} {M : Type u_5} [AddMonoid M] (f : α → M) (n : ℕ) :

(Function.support fun (x : α) => n • f x) ⊆ Function.support f

source

theorem Function.mulSupport_pow {α : Type u_1} {M : Type u_5} [Monoid M] (f : α → M) (n : ℕ) :

(Function.mulSupport fun (x : α) => f x ^ n) ⊆ Function.mulSupport f

source

@[simp]

theorem Function.support_neg {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f : α → G) :

(Function.support fun (x : α) => -f x) = Function.support f

source

@[simp]

theorem Function.mulSupport_inv {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f : α → G) :

(Function.mulSupport fun (x : α) => (f x)⁻¹) = Function.mulSupport f

source

@[simp]

theorem Function.support_neg' {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f : α → G) :

Function.support (-f) = Function.support f

source

@[simp]

theorem Function.mulSupport_inv' {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f : α → G) :

Function.mulSupport f⁻¹ = Function.mulSupport f

source

theorem Function.support_add_neg {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f : α → G) (g : α → G) :

(Function.support fun (x : α) => f x + -g x) ⊆ Function.support f ∪ Function.support g

source

theorem Function.mulSupport_mul_inv {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f : α → G) (g : α → G) :

(Function.mulSupport fun (x : α) => f x * (g x)⁻¹) ⊆ Function.mulSupport f ∪ Function.mulSupport g

source

theorem Function.support_sub {α : Type u_1} {G : Type u_9} [SubtractionMonoid G] (f : α → G) (g : α → G) :

(Function.support fun (x : α) => f x - g x) ⊆ Function.support f ∪ Function.support g

source

theorem Function.mulSupport_div {α : Type u_1} {G : Type u_9} [DivisionMonoid G] (f : α → G) (g : α → G) :

(Function.mulSupport fun (x : α) => f x / g x) ⊆ Function.mulSupport f ∪ Function.mulSupport 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 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 Pi.support_single_subset {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} {b : B} :

Function.support (Pi.single a b) ⊆ {a}

source

theorem Pi.mulSupport_mulSingle_subset {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} {b : B} :

Function.mulSupport (Pi.mulSingle a b) ⊆ {a}

source

theorem Pi.support_single_zero {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} :

Function.support (Pi.single a 0) = ∅

source

theorem Pi.mulSupport_mulSingle_one {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} :

Function.mulSupport (Pi.mulSingle a 1) = ∅

source

@[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) :

Function.support (Pi.single a b) = {a}

source

@[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) :

Function.mulSupport (Pi.mulSingle a b) = {a}

source

theorem Pi.support_single {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {a : A} {b : B} [DecidableEq B] :

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

source

theorem Pi.mulSupport_mulSingle {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {a : A} {b : B} [DecidableEq B] :

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

source

theorem Pi.support_single_disjoint {A : Type u_1} {B : Type u_2} [DecidableEq A] [Zero B] {b : B} {b' : B} (hb : b ≠ 0) (hb' : b' ≠ 0) {i : A} {j : A} :

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

source

theorem Pi.mulSupport_mulSingle_disjoint {A : Type u_1} {B : Type u_2} [DecidableEq A] [One B] {b : B} {b' : B} (hb : b ≠ 1) (hb' : b' ≠ 1) {i : A} {j : A} :

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

Documentation

Mathlib.Algebra.Group.Support

Support of a function #