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}.
mulSupport of a function is the set of points x such that 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_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_sup
{α : Type u_1}
{M : Type u_5}
[Zero M]
[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_1}
{M : Type u_5}
[One M]
[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_1}
{M : Type u_5}
[Zero M]
[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_1}
{M : Type u_5}
[One M]
[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_1}
{M : Type u_5}
[Zero M]
[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_1}
{M : Type u_5}
[One M]
[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_1}
{M : Type u_5}
[Zero M]
[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_1}
{M : Type u_5}
[One M]
[LinearOrder M]
(f : α → M)
(g : α → M)
:
(Function.mulSupport fun x => min (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
theorem
Function.support_iSup
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[Zero M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.support fun x => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.support (f i)
theorem
Function.mulSupport_iSup
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[One M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.mulSupport fun x => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.mulSupport (f i)
theorem
Function.support_iInf
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[Zero M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.support fun x => ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.support (f i)
theorem
Function.mulSupport_iInf
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[One M]
[ConditionallyCompleteLattice M]
[Nonempty ι]
(f : ι → α → M)
:
(Function.mulSupport fun x => ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), Function.mulSupport (f i)
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).fst) ∪ Function.support fun x => (f x).snd
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).fst) ∪ Function.mulSupport fun x => (f x).snd
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
@[simp]
theorem
Function.support_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[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_5}
[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_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_nat_cast
{α : Type u_1}
{R : Type u_8}
[AddMonoidWithOne R]
[CharZero R]
{n : ℕ}
(hn : n ≠ 0)
:
Function.support ↑n = Set.univ
theorem
Function.mulSupport_nat_cast
{α : Type u_1}
{R : Type u_8}
[AddMonoidWithOne R]
[CharZero R]
{n : ℕ}
(hn : n ≠ 1)
:
Function.mulSupport ↑n = Set.univ
theorem
Function.support_int_cast
{α : Type u_1}
{R : Type u_8}
[AddGroupWithOne R]
[CharZero R]
{n : ℤ}
(hn : n ≠ 0)
:
Function.support ↑n = Set.univ
theorem
Function.mulSupport_int_cast
{α : Type u_1}
{R : Type u_8}
[AddGroupWithOne R]
[CharZero R]
{n : ℤ}
(hn : n ≠ 1)
:
Function.mulSupport ↑n = Set.univ
theorem
Function.support_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_8}
[Zero R]
[Zero M]
[SMulWithZero R M]
[NoZeroSMulDivisors R M]
(f : α → R)
(g : α → M)
:
Function.support (f • g) = Function.support f ∩ Function.support g
@[simp]
theorem
Function.support_mul
{α : Type u_1}
{R : Type u_8}
[MulZeroClass R]
[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_1}
{R : Type u_8}
[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_1}
{R : Type u_8}
[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_1}
{A : Type u_3}
{B : Type u_4}
[AddMonoid A]
[Monoid B]
[DistribMulAction B A]
(b : B)
(f : α → A)
:
Function.support (b • f) ⊆ Function.support f
theorem
Function.support_smul_subset_left
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[Zero M]
[Zero β]
[SMulWithZero M β]
(f : α → M)
(g : α → β)
:
Function.support (f • g) ⊆ Function.support f
theorem
Function.support_const_smul_of_ne_zero
{α : Type u_1}
{M : Type u_5}
{R : Type u_8}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[NoZeroSMulDivisors R M]
(c : R)
(g : α → M)
(hc : c ≠ 0)
:
Function.support (c • g) = Function.support g
@[simp]
theorem
Function.support_inv
{α : Type u_1}
{G₀ : Type u_12}
[GroupWithZero G₀]
(f : α → G₀)
:
(Function.support fun x => (f x)⁻¹) = Function.support f
@[simp]
theorem
Function.support_div
{α : Type u_1}
{G₀ : Type u_12}
[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_1}
{β : Type u_2}
{M : Type u_5}
[AddCommMonoid M]
(s : Finset α)
(f : α → β → M)
:
(Function.support fun x => Finset.sum s fun i => f i x) ⊆ ⋃ (i : α) (_ : i ∈ s), Function.support (f i)
theorem
Function.mulSupport_prod
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[CommMonoid M]
(s : Finset α)
(f : α → β → M)
:
(Function.mulSupport fun x => Finset.prod s fun i => f i x) ⊆ ⋃ (i : α) (_ : i ∈ s), Function.mulSupport (f i)
theorem
Function.support_prod_subset
{α : Type u_1}
{β : Type u_2}
{A : Type u_3}
[CommMonoidWithZero A]
(s : Finset α)
(f : α → β → A)
:
(Function.support fun x => Finset.prod s fun i => f i x) ⊆ ⋂ (i : α) (_ : i ∈ s), Function.support (f i)
theorem
Function.support_prod
{α : Type u_1}
{β : Type u_2}
{A : Type u_3}
[CommMonoidWithZero A]
[NoZeroDivisors A]
[Nontrivial A]
(s : Finset α)
(f : α → β → A)
:
(Function.support fun x => Finset.prod s fun i => f i x) = ⋂ (i : α) (_ : i ∈ s), Function.support (f i)
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