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}.
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
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
theorem
Function.support_eq_preimage
{α : Type u_1}
{M : Type u_5}
[Zero M]
(f : α → M)
:
Function.support f = f ⁻¹' {0}ᶜ
theorem
Function.mulSupport_eq_preimage
{α : Type u_1}
{M : Type u_5}
[One M]
(f : α → M)
:
Function.mulSupport f = f ⁻¹' {1}ᶜ
theorem
Function.nmem_support
{α : Type u_1}
{M : Type u_5}
[Zero M]
{f : α → M}
{x : α}
:
x ∉ Function.support f ↔ f x = 0
theorem
Function.nmem_mulSupport
{α : Type u_1}
{M : Type u_5}
[One M]
{f : α → M}
{x : α}
:
x ∉ Function.mulSupport f ↔ f x = 1
theorem
Function.compl_support
{α : Type u_1}
{M : Type u_5}
[Zero M]
{f : α → M}
:
(Function.support f)ᶜ = {x : α | f x = 0}
theorem
Function.compl_mulSupport
{α : Type u_1}
{M : Type u_5}
[One M]
{f : α → M}
:
(Function.mulSupport f)ᶜ = {x : α | f x = 1}
@[simp]
theorem
Function.mem_support
{α : Type u_1}
{M : Type u_5}
[Zero M]
{f : α → M}
{x : α}
:
x ∈ Function.support f ↔ f x ≠ 0
@[simp]
theorem
Function.mem_mulSupport
{α : Type u_1}
{M : Type u_5}
[One M]
{f : α → M}
{x : α}
:
x ∈ Function.mulSupport f ↔ f x ≠ 1
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
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
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
abbrev
Function.ext_iff_support.match_1
{α : Type u_1}
{M : Type u_2}
[Zero M]
{f : α → M}
{g : α → M}
(motive : (Function.support f = Function.support g ∧ ∀ x ∈ Function.support f, f x = g x) → Prop)
:
∀ (x : Function.support f = Function.support g ∧ ∀ x ∈ Function.support f, f x = g x),
(∀ (h₁ : Function.support f = Function.support g) (h₂ : ∀ x ∈ Function.support f, f x = g x), motive ⋯) → motive x
Equations
- ⋯ = ⋯
Instances For
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
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)
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)
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}
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}
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)
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)
theorem
Function.support_extend_zero_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[Zero N]
{f : α → M}
{g : α → N}
:
Function.support (Function.extend f g 0) ⊆ f '' Function.support g
theorem
Function.mulSupport_extend_one_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[One N]
{f : α → M}
{g : α → N}
:
Function.mulSupport (Function.extend f g 1) ⊆ f '' Function.mulSupport g
theorem
Function.support_extend_zero
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[Zero N]
{f : α → M}
{g : α → N}
(hf : Function.Injective f)
:
Function.support (Function.extend f g 0) = f '' Function.support g
theorem
Function.mulSupport_extend_one
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[One N]
{f : α → M}
{g : α → N}
(hf : Function.Injective f)
:
Function.mulSupport (Function.extend f g 1) = f '' Function.mulSupport g
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
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
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
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
@[simp]
theorem
Function.support_eq_empty_iff
{α : Type u_1}
{M : Type u_5}
[Zero M]
{f : α → M}
:
Function.support f = ∅ ↔ f = 0
@[simp]
theorem
Function.mulSupport_eq_empty_iff
{α : Type u_1}
{M : Type u_5}
[One M]
{f : α → M}
:
Function.mulSupport f = ∅ ↔ f = 1
@[simp]
theorem
Function.support_nonempty_iff
{α : Type u_1}
{M : Type u_5}
[Zero M]
{f : α → M}
:
Set.Nonempty (Function.support f) ↔ f ≠ 0
@[simp]
theorem
Function.mulSupport_nonempty_iff
{α : Type u_1}
{M : Type u_5}
[One M]
{f : α → M}
:
Set.Nonempty (Function.mulSupport f) ↔ f ≠ 1
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)
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)
@[simp]
@[simp]
@[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]
:
(Function.mulSupport fun (x : α) => 1) = ∅
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 : 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
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 : 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
theorem
Function.support_comp_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[Zero M]
[Zero N]
{g : M → N}
(hg : g 0 = 0)
(f : α → M)
:
Function.support (g ∘ f) ⊆ Function.support f
theorem
Function.mulSupport_comp_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[One M]
[One N]
{g : M → N}
(hg : g 1 = 1)
(f : α → M)
:
Function.mulSupport (g ∘ f) ⊆ Function.mulSupport f
theorem
Function.support_subset_comp
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[Zero M]
[Zero N]
{g : M → N}
(hg : ∀ {x : M}, g x = 0 → x = 0)
(f : α → M)
:
Function.support f ⊆ Function.support (g ∘ f)
theorem
Function.mulSupport_subset_comp
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[One M]
[One N]
{g : M → N}
(hg : ∀ {x : M}, g x = 1 → x = 1)
(f : α → M)
:
Function.mulSupport f ⊆ Function.mulSupport (g ∘ f)
theorem
Function.support_comp_eq
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[Zero M]
[Zero N]
(g : M → N)
(hg : ∀ {x : M}, g x = 0 ↔ x = 0)
(f : α → M)
:
Function.support (g ∘ f) = Function.support f
theorem
Function.mulSupport_comp_eq
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[One M]
[One N]
(g : M → N)
(hg : ∀ {x : M}, g x = 1 ↔ x = 1)
(f : α → M)
:
Function.mulSupport (g ∘ f) = Function.mulSupport f
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
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
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)) = Function.support f ∪ Function.support g
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)) = Function.mulSupport f ∪ Function.mulSupport g
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 f = (Function.support fun (x : α) => (f x).1) ∪ Function.support fun (x : α) => (f x).2
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 f = (Function.mulSupport fun (x : α) => (f x).1) ∪ Function.mulSupport fun (x : α) => (f x).2
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
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
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
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
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
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
@[simp]
theorem
Function.support_neg
{α : Type u_1}
{G : Type u_10}
[SubtractionMonoid G]
(f : α → G)
:
(Function.support fun (x : α) => -f x) = Function.support f
@[simp]
theorem
Function.mulSupport_inv
{α : Type u_1}
{G : Type u_10}
[DivisionMonoid G]
(f : α → G)
:
(Function.mulSupport fun (x : α) => (f x)⁻¹) = Function.mulSupport f
@[simp]
@[simp]
theorem
Function.support_add_neg
{α : Type u_1}
{G : Type u_10}
[SubtractionMonoid G]
(f : α → G)
(g : α → G)
:
(Function.support fun (x : α) => f x + -g x) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_mul_inv
{α : Type u_1}
{G : Type u_10}
[DivisionMonoid G]
(f : α → G)
(g : α → G)
:
(Function.mulSupport fun (x : α) => f x * (g x)⁻¹) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_sub
{α : Type u_1}
{G : Type u_10}
[SubtractionMonoid G]
(f : α → G)
(g : α → G)
:
(Function.support fun (x : α) => f x - g x) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_div
{α : Type u_1}
{G : Type u_10}
[DivisionMonoid G]
(f : α → G)
(g : α → G)
:
(Function.mulSupport fun (x : α) => f x / g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
@[simp]
theorem
Function.support_one
{α : Type u_1}
(R : Type u_8)
[Zero R]
[One R]
[NeZero 1]
:
Function.support 1 = Set.univ
@[simp]
theorem
Function.mulSupport_zero
{α : Type u_1}
(R : Type u_8)
[Zero R]
[One R]
[NeZero 1]
:
Function.mulSupport 0 = Set.univ
theorem
Function.support_mul_subset_left
{α : Type u_1}
{M : Type u_5}
[MulZeroClass M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => f x * g x) ⊆ Function.support f
theorem
Function.support_mul_subset_right
{α : Type u_1}
{M : Type u_5}
[MulZeroClass M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => f x * g x) ⊆ Function.support g
@[simp]
theorem
Function.support_mul
{α : Type u_1}
{M : Type u_5}
[MulZeroClass M]
[NoZeroDivisors M]
(f : α → M)
(g : α → M)
:
(Function.support fun (x : α) => f x * g x) = Function.support f ∩ Function.support g
@[simp]
theorem
Function.support_mul'
{α : Type u_1}
{M : Type u_5}
[MulZeroClass M]
[NoZeroDivisors M]
(f : α → M)
(g : α → M)
:
Function.support (f * g) = Function.support f ∩ Function.support g
@[simp]
theorem
Function.support_pow
{α : Type u_1}
{M : Type u_5}
[MonoidWithZero M]
[NoZeroDivisors M]
{n : ℕ}
(f : α → M)
(hn : n ≠ 0)
:
(Function.support fun (a : α) => f a ^ n) = Function.support f
@[simp]
theorem
Function.support_pow'
{α : Type u_1}
{M : Type u_5}
[MonoidWithZero M]
[NoZeroDivisors M]
{n : ℕ}
(f : α → M)
(hn : n ≠ 0)
:
Function.support (f ^ n) = Function.support f
@[simp]
theorem
Function.support_inv
{α : Type u_1}
{G₀ : Type u_12}
[GroupWithZero G₀]
(f : α → G₀)
:
(Function.support fun (a : α) => (f a)⁻¹) = Function.support f
@[simp]
@[simp]
theorem
Function.support_div
{α : Type u_1}
{G₀ : Type u_12}
[GroupWithZero G₀]
(f : α → G₀)
(g : α → G₀)
:
(Function.support fun (a : α) => f a / g a) = Function.support f ∩ Function.support g
@[simp]
theorem
Function.support_div'
{α : Type u_1}
{G₀ : Type u_12}
[GroupWithZero G₀]
(f : α → G₀)
(g : α → G₀)
:
Function.support (f / g) = Function.support f ∩ Function.support g
theorem
Function.mulSupport_one_add
{α : Type u_1}
{R : Type u_8}
[One R]
[AddLeftCancelMonoid R]
(f : α → R)
:
(Function.mulSupport fun (x : α) => 1 + f x) = Function.support f
theorem
Function.mulSupport_one_add'
{α : Type u_1}
{R : Type u_8}
[One R]
[AddLeftCancelMonoid R]
(f : α → R)
:
Function.mulSupport (1 + f) = Function.support f
theorem
Function.mulSupport_add_one
{α : Type u_1}
{R : Type u_8}
[One R]
[AddRightCancelMonoid R]
(f : α → R)
:
(Function.mulSupport fun (x : α) => f x + 1) = Function.support f
theorem
Function.mulSupport_add_one'
{α : Type u_1}
{R : Type u_8}
[One R]
[AddRightCancelMonoid R]
(f : α → R)
:
Function.mulSupport (f + 1) = Function.support f
theorem
Function.mulSupport_one_sub'
{α : Type u_1}
{R : Type u_8}
[One R]
[AddGroup R]
(f : α → R)
:
Function.mulSupport (1 - f) = Function.support f
theorem
Function.mulSupport_one_sub
{α : Type u_1}
{R : Type u_8}
[One R]
[AddGroup R]
(f : α → R)
:
(Function.mulSupport fun (x : α) => 1 - f x) = Function.support f
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))
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))
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}
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}
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) = ∅
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) = ∅
@[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}
@[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}
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}
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}
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
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