Support of a function #
In this file we define Function.support f = {x | f x ≠ 0}≠ 0}
and prove its basic properties.
We also define Function.mulSupport f = {x | f x ≠ 1}≠ 1}
.
mulSupport
of a function is the set of points x
such that f x ≠ 1≠ 1
.
Equations
- Function.mulSupport f = { x | f x ≠ 1 }
theorem
Function.support_eq_preimage
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(f : α → M)
:
Function.support f = f ⁻¹' {0}ᶜ
theorem
Function.mulSupport_eq_preimage
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(f : α → M)
:
Function.mulSupport f = f ⁻¹' {1}ᶜ
theorem
Function.compl_support
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{f : α → M}
:
Function.support fᶜ = { x | f x = 0 }
theorem
Function.compl_mulSupport
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{f : α → M}
:
Function.mulSupport fᶜ = { x | f x = 1 }
@[simp]
theorem
Function.mem_support
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{f : α → M}
{x : α}
:
x ∈ Function.support f ↔ f x ≠ 0
@[simp]
theorem
Function.mem_mulSupport
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{f : α → M}
{x : α}
:
x ∈ Function.mulSupport f ↔ f x ≠ 1
@[simp]
theorem
Function.support_nonempty_iff
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{f : α → M}
:
Set.Nonempty (Function.support f) ↔ f ≠ 0
@[simp]
theorem
Function.mulSupport_nonempty_iff
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{f : α → M}
:
Set.Nonempty (Function.mulSupport f) ↔ f ≠ 1
@[simp]
@[simp]
@[simp]
theorem
Function.support_zero
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
:
(Function.support fun x => 0) = ∅
@[simp]
theorem
Function.mulSupport_one
{α : Type u_1}
{M : Type u_2}
[inst : One M]
:
(Function.mulSupport fun x => 1) = ∅
theorem
Function.support_const
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
{c : M}
(hc : c ≠ 0)
:
(Function.support fun x => c) = Set.univ
theorem
Function.mulSupport_const
{α : Type u_2}
{M : Type u_1}
[inst : One M]
{c : M}
(hc : c ≠ 1)
:
(Function.mulSupport fun x => c) = Set.univ
theorem
Function.support_binop_subset
{α : Type u_4}
{M : Type u_2}
{N : Type u_3}
{P : Type u_1}
[inst : Zero M]
[inst : Zero N]
[inst : 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_4}
{M : Type u_2}
{N : Type u_3}
{P : Type u_1}
[inst : One M]
[inst : One N]
[inst : 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_sup
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
[inst : SemilatticeSup M]
(f : α → M)
(g : α → M)
:
(Function.support fun x => f x ⊔ g x) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_sup
{α : Type u_2}
{M : Type u_1}
[inst : One M]
[inst : SemilatticeSup M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun x => f x ⊔ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_inf
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
[inst : SemilatticeInf M]
(f : α → M)
(g : α → M)
:
(Function.support fun x => f x ⊓ g x) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_inf
{α : Type u_2}
{M : Type u_1}
[inst : One M]
[inst : SemilatticeInf M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun x => f x ⊓ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_max
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
[inst : LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.support fun x => max (f x) (g x)) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_max
{α : Type u_2}
{M : Type u_1}
[inst : One M]
[inst : LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun x => max (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_min
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
[inst : LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.support fun x => min (f x) (g x)) ⊆ Function.support f ∪ Function.support g
theorem
Function.mulSupport_min
{α : Type u_2}
{M : Type u_1}
[inst : One M]
[inst : LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun x => min (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_supᵢ
{α : Type u_3}
{M : Type u_1}
{ι : Sort u_2}
[inst : Zero M]
[inst : ConditionallyCompleteLattice M]
[inst : Nonempty ι]
(f : ι → α → M)
:
(Function.support fun x => ⨆ i, f i x) ⊆ Set.unionᵢ fun i => Function.support (f i)
theorem
Function.mulSupport_supᵢ
{α : Type u_3}
{M : Type u_1}
{ι : Sort u_2}
[inst : One M]
[inst : ConditionallyCompleteLattice M]
[inst : Nonempty ι]
(f : ι → α → M)
:
(Function.mulSupport fun x => ⨆ i, f i x) ⊆ Set.unionᵢ fun i => Function.mulSupport (f i)
theorem
Function.support_infᵢ
{α : Type u_3}
{M : Type u_1}
{ι : Sort u_2}
[inst : Zero M]
[inst : ConditionallyCompleteLattice M]
[inst : Nonempty ι]
(f : ι → α → M)
:
(Function.support fun x => ⨅ i, f i x) ⊆ Set.unionᵢ fun i => Function.support (f i)
theorem
Function.mulSupport_infᵢ
{α : Type u_3}
{M : Type u_1}
{ι : Sort u_2}
[inst : One M]
[inst : ConditionallyCompleteLattice M]
[inst : Nonempty ι]
(f : ι → α → M)
:
(Function.mulSupport fun x => ⨅ i, f i x) ⊆ Set.unionᵢ fun i => Function.mulSupport (f i)
theorem
Function.support_comp_subset
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : 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_3}
{M : Type u_2}
{N : Type u_1}
[inst : One M]
[inst : 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_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : 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_3}
{M : Type u_2}
{N : Type u_1}
[inst : One M]
[inst : 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_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : 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_3}
{M : Type u_2}
{N : Type u_1}
[inst : One M]
[inst : 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_3}
{M : Type u_2}
[inst : Zero M]
(g : β → M)
(f : α → β)
:
Function.support (g ∘ f) = f ⁻¹' Function.support g
theorem
Function.mulSupport_comp_eq_preimage
{α : Type u_1}
{β : Type u_3}
{M : Type u_2}
[inst : One M]
(g : β → M)
(f : α → β)
:
Function.mulSupport (g ∘ f) = f ⁻¹' Function.mulSupport g
theorem
Function.support_prod_mk
{α : Type u_1}
{M : Type u_3}
{N : Type u_2}
[inst : Zero M]
[inst : 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_3}
{N : Type u_2}
[inst : One M]
[inst : 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_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : Zero N]
(f : α → M × N)
:
Function.support f = (Function.support fun x => (f x).fst) ∪ Function.support fun x => (f x).snd
theorem
Function.mulSupport_prod_mk'
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : One M]
[inst : One N]
(f : α → M × N)
:
Function.mulSupport f = (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_3}
[inst : 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_3}
[inst : One M]
(f : α × β → M)
(a : α)
:
(Function.mulSupport fun b => f (a, b)) ⊆ Prod.snd '' Function.mulSupport f
@[simp]
theorem
Function.support_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[inst : Zero M]
(f : α × β → M)
(a : α)
(h : Set.Finite (Function.support f))
:
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_3}
[inst : One M]
(f : α × β → M)
(a : α)
(h : Set.Finite (Function.mulSupport f))
:
Set.Finite (Function.mulSupport fun b => f (a, b))
theorem
Function.support_add
{α : Type u_2}
{M : Type u_1}
[inst : 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_2}
{M : Type u_1}
[inst : 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_2}
{M : Type u_1}
[inst : AddMonoid M]
(f : α → M)
(n : ℕ)
:
(Function.support fun x => n • f x) ⊆ Function.support f
theorem
Function.mulSupport_pow
{α : Type u_2}
{M : Type u_1}
[inst : 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_2}
[inst : SubtractionMonoid G]
(f : α → G)
:
(Function.support fun x => -f x) = Function.support f
@[simp]
theorem
Function.mulSupport_inv
{α : Type u_1}
{G : Type u_2}
[inst : DivisionMonoid G]
(f : α → G)
:
(Function.mulSupport fun x => (f x)⁻¹) = Function.mulSupport f
@[simp]
theorem
Function.support_neg'
{α : Type u_1}
{G : Type u_2}
[inst : SubtractionMonoid G]
(f : α → G)
:
@[simp]
theorem
Function.mulSupport_inv'
{α : Type u_1}
{G : Type u_2}
[inst : DivisionMonoid G]
(f : α → G)
:
theorem
Function.support_add_neg
{α : Type u_1}
{G : Type u_2}
[inst : 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_2}
[inst : 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_2}
[inst : 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_2}
[inst : DivisionMonoid G]
(f : α → G)
(g : α → G)
:
(Function.mulSupport fun x => f x / g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_smul
{α : Type u_3}
{M : Type u_2}
{R : Type u_1}
[inst : Zero R]
[inst : Zero M]
[inst : SMulWithZero R M]
[inst : NoZeroSMulDivisors R M]
(f : α → R)
(g : α → M)
:
Function.support (f • g) = Function.support f ∩ Function.support g
@[simp]
theorem
Function.support_mul
{α : Type u_2}
{R : Type u_1}
[inst : MulZeroClass R]
[inst : NoZeroDivisors R]
(f : α → R)
(g : α → R)
:
(Function.support fun x => f x * g x) = Function.support f ∩ Function.support g
theorem
Function.support_mul_subset_left
{α : Type u_2}
{R : Type u_1}
[inst : MulZeroClass R]
(f : α → R)
(g : α → R)
:
(Function.support fun x => f x * g x) ⊆ Function.support f
theorem
Function.support_mul_subset_right
{α : Type u_2}
{R : Type u_1}
[inst : MulZeroClass R]
(f : α → R)
(g : α → R)
:
(Function.support fun x => f x * g x) ⊆ Function.support g
theorem
Function.support_smul_subset_right
{α : Type u_3}
{A : Type u_1}
{B : Type u_2}
[inst : AddMonoid A]
[inst : Monoid B]
[inst : DistribMulAction B A]
(b : B)
(f : α → A)
:
Function.support (b • f) ⊆ Function.support f
theorem
Function.support_smul_subset_left
{α : Type u_3}
{β : Type u_2}
{M : Type u_1}
[inst : Zero M]
[inst : Zero β]
[inst : SMulWithZero M β]
(f : α → M)
(g : α → β)
:
Function.support (f • g) ⊆ Function.support f
theorem
Function.support_const_smul_of_ne_zero
{α : Type u_3}
{M : Type u_2}
{R : Type u_1}
[inst : Semiring R]
[inst : AddCommMonoid M]
[inst : Module R M]
[inst : NoZeroSMulDivisors R M]
(c : R)
(g : α → M)
(hc : c ≠ 0)
:
Function.support (c • g) = Function.support g
@[simp]
theorem
Function.support_inv
{α : Type u_2}
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
(f : α → G₀)
:
(Function.support fun x => (f x)⁻¹) = Function.support f
@[simp]
theorem
Function.support_div
{α : Type u_2}
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
(f : α → G₀)
(g : α → G₀)
:
(Function.support fun x => f x / g x) = Function.support f ∩ Function.support g
theorem
Function.support_sum
{α : Type u_2}
{β : Type u_3}
{M : Type u_1}
[inst : AddCommMonoid M]
(s : Finset α)
(f : α → β → M)
:
(Function.support fun x => Finset.sum s fun i => f i x) ⊆ Set.unionᵢ fun i => Set.unionᵢ fun h => Function.support (f i)
theorem
Function.mulSupport_prod
{α : Type u_2}
{β : Type u_3}
{M : Type u_1}
[inst : CommMonoid M]
(s : Finset α)
(f : α → β → M)
:
(Function.mulSupport fun x => Finset.prod s fun i => f i x) ⊆ Set.unionᵢ fun i => Set.unionᵢ fun h => Function.mulSupport (f i)
theorem
Function.support_prod_subset
{α : Type u_2}
{β : Type u_3}
{A : Type u_1}
[inst : CommMonoidWithZero A]
(s : Finset α)
(f : α → β → A)
:
(Function.support fun x => Finset.prod s fun i => f i x) ⊆ Set.interᵢ fun i => Set.interᵢ fun h => Function.support (f i)
theorem
Function.support_prod
{α : Type u_2}
{β : Type u_3}
{A : Type u_1}
[inst : CommMonoidWithZero A]
[inst : NoZeroDivisors A]
[inst : Nontrivial A]
(s : Finset α)
(f : α → β → A)
:
(Function.support fun x => Finset.prod s fun i => f i x) = Set.interᵢ fun i => Set.interᵢ fun h => Function.support (f i)
theorem
Function.mulSupport_one_add
{α : Type u_2}
{R : Type u_1}
[inst : One R]
[inst : AddLeftCancelMonoid R]
(f : α → R)
:
(Function.mulSupport fun x => 1 + f x) = Function.support f
theorem
Function.mulSupport_one_add'
{α : Type u_2}
{R : Type u_1}
[inst : One R]
[inst : AddLeftCancelMonoid R]
(f : α → R)
:
Function.mulSupport (1 + f) = Function.support f
theorem
Function.mulSupport_add_one
{α : Type u_2}
{R : Type u_1}
[inst : One R]
[inst : AddRightCancelMonoid R]
(f : α → R)
:
(Function.mulSupport fun x => f x + 1) = Function.support f
theorem
Function.mulSupport_add_one'
{α : Type u_2}
{R : Type u_1}
[inst : One R]
[inst : AddRightCancelMonoid R]
(f : α → R)
:
Function.mulSupport (f + 1) = Function.support f
theorem
Function.mulSupport_one_sub'
{α : Type u_2}
{R : Type u_1}
[inst : One R]
[inst : AddGroup R]
(f : α → R)
:
Function.mulSupport (1 - f) = Function.support f
theorem
Function.mulSupport_one_sub
{α : Type u_2}
{R : Type u_1}
[inst : One R]
[inst : AddGroup R]
(f : α → R)
:
(Function.mulSupport fun x => 1 - f x) = Function.support f
theorem
Pi.support_single_subset
{A : Type u_1}
{B : Type u_2}
[inst : DecidableEq A]
[inst : 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}
[inst : DecidableEq A]
[inst : 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}
[inst : DecidableEq A]
[inst : Zero B]
{a : A}
:
Function.support (Pi.single a 0) = ∅
theorem
Pi.mulSupport_mulSingle_one
{A : Type u_1}
{B : Type u_2}
[inst : DecidableEq A]
[inst : One B]
{a : A}
:
Function.mulSupport (Pi.mulSingle a 1) = ∅
@[simp]
theorem
Pi.support_single_of_ne
{A : Type u_2}
{B : Type u_1}
[inst : DecidableEq A]
[inst : 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_2}
{B : Type u_1}
[inst : DecidableEq A]
[inst : One B]
{a : A}
{b : B}
(h : b ≠ 1)
:
Function.mulSupport (Pi.mulSingle a b) = {a}
theorem
Pi.support_single
{A : Type u_2}
{B : Type u_1}
[inst : DecidableEq A]
[inst : Zero B]
{a : A}
{b : B}
[inst : DecidableEq B]
:
Function.support (Pi.single a b) = if b = 0 then ∅ else {a}
theorem
Pi.mulSupport_mulSingle
{A : Type u_2}
{B : Type u_1}
[inst : DecidableEq A]
[inst : One B]
{a : A}
{b : B}
[inst : DecidableEq B]
:
Function.mulSupport (Pi.mulSingle a b) = if b = 1 then ∅ else {a}
theorem
Pi.support_single_disjoint
{A : Type u_2}
{B : Type u_1}
[inst : DecidableEq A]
[inst : 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_2}
{B : Type u_1}
[inst : DecidableEq A]
[inst : 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