Documentation

Mathlib.Algebra.Support

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

source
ink
def Function.support {α : Type u_1} {A : Type u_2} [inst : Zero A] (f : α → A) :
Set α

support of a function is the set of points x such that f x ≠ 0≠ 0.

Equations
source
ink
def Function.mulSupport {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M) :
Set α

mulSupport of a function is the set of points x such that f x ≠ 1≠ 1.

Equations
source
ink
theorem Function.support_eq_preimage {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M) :
Function.support f = f ⁻¹' {0}ᶜ
source
ink
theorem Function.mulSupport_eq_preimage {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M) :
Function.mulSupport f = f ⁻¹' {1}ᶜ
source
ink
theorem Function.nmem_support {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} {x : α} :
¬x ∈ Function.support f ↔ f x = 0
source
ink
theorem Function.nmem_mulSupport {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} {x : α} :
¬x ∈ Function.mulSupport f ↔ f x = 1
source
ink
theorem Function.compl_support {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} :
Function.support fᶜ = { x | f x = 0 }
source
ink
theorem Function.compl_mulSupport {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} :
Function.mulSupport fᶜ = { x | f x = 1 }
source
ink
@[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
source
ink
@[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
source
ink
@[simp]
theorem Function.support_subset_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} {s : Set α} :
Function.support f ⊆ s ↔ ∀ (x : α), f x ≠ 0 → x ∈ s
source
ink
@[simp]
theorem Function.mulSupport_subset_iff {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} {s : Set α} :
Function.mulSupport f ⊆ s ↔ ∀ (x : α), f x ≠ 1 → x ∈ s
source
ink
theorem Function.support_subset_iff' {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} {s : Set α} :
Function.support f ⊆ s ↔ ∀ (x : α), ¬x ∈ s → f x = 0
source
ink
theorem Function.mulSupport_subset_iff' {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} {s : Set α} :
Function.mulSupport f ⊆ s ↔ ∀ (x : α), ¬x ∈ s → f x = 1
source
ink
theorem Function.support_eq_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} {s : Set α} :
Function.support f = s ↔ (∀ (x : α), x ∈ s → f x ≠ 0) ∧ ∀ (x : α), ¬x ∈ s → f x = 0
source
ink
theorem Function.mulSupport_eq_iff {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} {s : Set α} :
Function.mulSupport f = s ↔ (∀ (x : α), x ∈ s → f x ≠ 1) ∧ ∀ (x : α), ¬x ∈ s → f x = 1
source
ink
theorem Function.support_disjoint_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} {s : Set α} :
Disjoint (Function.support f) s ↔ Set.EqOn f 0 s
source
ink
theorem Function.mulSupport_disjoint_iff {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} {s : Set α} :
Disjoint (Function.mulSupport f) s ↔ Set.EqOn f 1 s
source
ink
theorem Function.disjoint_support_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} {s : Set α} :
Disjoint s (Function.support f) ↔ Set.EqOn f 0 s
source
ink
theorem Function.disjoint_mulSupport_iff {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} {s : Set α} :
Disjoint s (Function.mulSupport f) ↔ Set.EqOn f 1 s
source
ink
@[simp]
theorem Function.support_eq_empty_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M} :
Function.support f = ∅ ↔ f = 0
source
ink
@[simp]
theorem Function.mulSupport_eq_empty_iff {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M} :
Function.mulSupport f = ∅ ↔ f = 1
source
ink
@[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
source
ink
@[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
source
ink
theorem Function.range_subset_insert_image_support {α : Type u_2} {M : Type u_1} [inst : Zero M] (f : α → M) :
Set.range f ⊆ insert 0 (f '' Function.support f)
source
ink
theorem Function.range_subset_insert_image_mulSupport {α : Type u_2} {M : Type u_1} [inst : One M] (f : α → M) :
Set.range f ⊆ insert 1 (f '' Function.mulSupport f)
source
ink
@[simp]
theorem Function.support_zero' {α : Type u_1} {M : Type u_2} [inst : Zero M] :
Function.support 0 = ∅
source
ink
@[simp]
theorem Function.mulSupport_one' {α : Type u_1} {M : Type u_2} [inst : One M] :
Function.mulSupport 1 = ∅
source
ink
@[simp]
theorem Function.support_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] :
(Function.support fun x => 0) = ∅
source
ink
@[simp]
theorem Function.mulSupport_one {α : Type u_1} {M : Type u_2} [inst : One M] :
(Function.mulSupport fun x => 1) = ∅
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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)
source
ink
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)
source
ink
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)
source
ink
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)
source
ink
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
source
ink
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
source
ink
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)
source
ink
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)
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
@[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))
source
ink
@[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))
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
@[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
source
ink
@[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
source
ink
@[simp]
theorem Function.support_neg' {α : Type u_1} {G : Type u_2} [inst : SubtractionMonoid G] (f : α → G) :
Function.support (-f) = Function.support f
source
ink
@[simp]
theorem Function.mulSupport_inv' {α : Type u_1} {G : Type u_2} [inst : DivisionMonoid G] (f : α → G) :
Function.mulSupport f⁻¹ = Function.mulSupport f
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
@[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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
@[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
source
ink
@[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
source
ink
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)
source
ink
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)
source
ink
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)
source
ink
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)
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
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
source
ink
theorem Set.image_inter_support_eq {α : Type u_2} {β : Type u_1} {M : Type u_3} [inst : Zero M] {f : α → M} {s : Set β} {g : β → α} :
g '' s ∩ Function.support f = g '' (s ∩ Function.support (f ∘ g))
source
ink
theorem Set.image_inter_mulSupport_eq {α : Type u_2} {β : Type u_1} {M : Type u_3} [inst : One M] {f : α → M} {s : Set β} {g : β → α} :
g '' s ∩ Function.mulSupport f = g '' (s ∩ Function.mulSupport (f ∘ g))
source
ink
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}
source
ink
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}
source
ink
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) = ∅
source
ink
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) = ∅
source
ink
@[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}
source
ink
@[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}
source
ink
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}
source
ink
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}
source
ink
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
source
ink
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