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.mul_support 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}
mul_support of a function is the set of points x such that f x ≠ 1.
Equations
- function.mul_support f = {x : α | f x ≠ 1}
theorem
function.support_eq_preimage
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α → M) :
function.support f = f ⁻¹' {0}ᶜ
theorem
function.mul_support_eq_preimage
{α : Type u_1}
{M : Type u_5}
[has_one M]
(f : α → M) :
function.mul_support f = f ⁻¹' {1}ᶜ
theorem
function.nmem_mul_support
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M}
{x : α} :
x ∉ function.mul_support f ↔ f x = 1
theorem
function.nmem_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{x : α} :
x ∉ function.support f ↔ f x = 0
theorem
function.compl_mul_support
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M} :
(function.mul_support f)ᶜ = {x : α | f x = 1}
theorem
function.compl_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M} :
(function.support f)ᶜ = {x : α | f x = 0}
@[simp]
theorem
function.mem_mul_support
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M}
{x : α} :
x ∈ function.mul_support f ↔ f x ≠ 1
@[simp]
theorem
function.mem_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{x : α} :
x ∈ function.support f ↔ f x ≠ 0
@[simp]
theorem
function.support_subset_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{s : set α} :
function.support f ⊆ s ↔ ∀ (x : α), f x ≠ 0 → x ∈ s
@[simp]
theorem
function.mul_support_subset_iff
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M}
{s : set α} :
function.mul_support f ⊆ s ↔ ∀ (x : α), f x ≠ 1 → x ∈ s
theorem
function.support_subset_iff'
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{s : set α} :
function.support f ⊆ s ↔ ∀ (x : α), x ∉ s → f x = 0
theorem
function.mul_support_subset_iff'
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M}
{s : set α} :
function.mul_support f ⊆ s ↔ ∀ (x : α), x ∉ s → f x = 1
theorem
function.support_disjoint_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{s : set α} :
disjoint (function.support f) s ↔ set.eq_on f 0 s
theorem
function.mul_support_disjoint_iff
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M}
{s : set α} :
disjoint (function.mul_support f) s ↔ set.eq_on f 1 s
theorem
function.disjoint_support_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{s : set α} :
disjoint s (function.support f) ↔ set.eq_on f 0 s
theorem
function.disjoint_mul_support_iff
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M}
{s : set α} :
disjoint s (function.mul_support f) ↔ set.eq_on f 1 s
@[simp]
theorem
function.mul_support_eq_empty_iff
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M} :
function.mul_support f = ∅ ↔ f = 1
@[simp]
theorem
function.support_eq_empty_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M} :
function.support f = ∅ ↔ f = 0
@[simp]
theorem
function.support_nonempty_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M} :
(function.support f).nonempty ↔ f ≠ 0
@[simp]
theorem
function.mul_support_nonempty_iff
{α : Type u_1}
{M : Type u_5}
[has_one M]
{f : α → M} :
(function.mul_support f).nonempty ↔ f ≠ 1
@[simp]
@[simp]
@[simp]
theorem
function.mul_support_one
{α : Type u_1}
{M : Type u_5}
[has_one M] :
function.mul_support (λ (x : α), 1) = ∅
@[simp]
theorem
function.support_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M] :
function.support (λ (x : α), 0) = ∅
theorem
function.mul_support_const
{α : Type u_1}
{M : Type u_5}
[has_one M]
{c : M}
(hc : c ≠ 1) :
function.mul_support (λ (x : α), c) = set.univ
theorem
function.support_const
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{c : M}
(hc : c ≠ 0) :
function.support (λ (x : α), c) = set.univ
theorem
function.mul_support_binop_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[has_one M]
[has_one N]
[has_one P]
(op : M → N → P)
(op1 : op 1 1 = 1)
(f : α → M)
(g : α → N) :
function.mul_support (λ (x : α), op (f x) (g x)) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_binop_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[has_zero M]
[has_zero N]
[has_zero P]
(op : M → N → P)
(op1 : op 0 0 = 0)
(f : α → M)
(g : α → N) :
function.support (λ (x : α), op (f x) (g x)) ⊆ function.support f ∪ function.support g
theorem
function.support_sup
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[semilattice_sup M]
(f g : α → M) :
function.support (λ (x : α), f x ⊔ g x) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_sup
{α : Type u_1}
{M : Type u_5}
[has_one M]
[semilattice_sup M]
(f g : α → M) :
function.mul_support (λ (x : α), f x ⊔ g x) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_inf
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[semilattice_inf M]
(f g : α → M) :
function.support (λ (x : α), f x ⊓ g x) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_inf
{α : Type u_1}
{M : Type u_5}
[has_one M]
[semilattice_inf M]
(f g : α → M) :
function.mul_support (λ (x : α), f x ⊓ g x) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.mul_support_max
{α : Type u_1}
{M : Type u_5}
[has_one M]
[linear_order M]
(f g : α → M) :
function.mul_support (λ (x : α), max (f x) (g x)) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_max
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[linear_order M]
(f g : α → M) :
function.support (λ (x : α), max (f x) (g x)) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_min
{α : Type u_1}
{M : Type u_5}
[has_one M]
[linear_order M]
(f g : α → M) :
function.mul_support (λ (x : α), min (f x) (g x)) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_min
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[linear_order M]
(f g : α → M) :
function.support (λ (x : α), min (f x) (g x)) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_supr
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[has_one M]
[conditionally_complete_lattice M]
[nonempty ι]
(f : ι → α → M) :
function.mul_support (λ (x : α), ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), function.mul_support (f i)
theorem
function.support_supr
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[has_zero M]
[conditionally_complete_lattice M]
[nonempty ι]
(f : ι → α → M) :
function.support (λ (x : α), ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), function.support (f i)
theorem
function.mul_support_infi
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[has_one M]
[conditionally_complete_lattice M]
[nonempty ι]
(f : ι → α → M) :
function.mul_support (λ (x : α), ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), function.mul_support (f i)
theorem
function.support_infi
{α : Type u_1}
{M : Type u_5}
{ι : Sort u_13}
[has_zero M]
[conditionally_complete_lattice M]
[nonempty ι]
(f : ι → α → M) :
function.support (λ (x : α), ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), function.support (f i)
theorem
function.mul_support_comp_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_one M]
[has_one N]
{g : M → N}
(hg : g 1 = 1)
(f : α → M) :
function.mul_support (g ∘ f) ⊆ function.mul_support f
theorem
function.support_comp_subset
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_zero M]
[has_zero N]
{g : M → N}
(hg : g 0 = 0)
(f : α → M) :
function.support (g ∘ f) ⊆ function.support f
theorem
function.mul_support_subset_comp
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_one M]
[has_one N]
{g : M → N}
(hg : ∀ {x : M}, g x = 1 → x = 1)
(f : α → M) :
function.mul_support f ⊆ function.mul_support (g ∘ f)
theorem
function.support_subset_comp
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_zero M]
[has_zero N]
{g : M → N}
(hg : ∀ {x : M}, g x = 0 → x = 0)
(f : α → M) :
function.support f ⊆ function.support (g ∘ f)
theorem
function.mul_support_comp_eq
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_one M]
[has_one N]
(g : M → N)
(hg : ∀ {x : M}, g x = 1 ↔ x = 1)
(f : α → M) :
function.mul_support (g ∘ f) = function.mul_support f
theorem
function.support_comp_eq
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_zero M]
[has_zero N]
(g : M → N)
(hg : ∀ {x : M}, g x = 0 ↔ x = 0)
(f : α → M) :
function.support (g ∘ f) = function.support f
theorem
function.support_comp_eq_preimage
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(g : β → M)
(f : α → β) :
function.support (g ∘ f) = f ⁻¹' function.support g
theorem
function.mul_support_comp_eq_preimage
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_one M]
(g : β → M)
(f : α → β) :
function.mul_support (g ∘ f) = f ⁻¹' function.mul_support g
theorem
function.support_prod_mk
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_zero M]
[has_zero N]
(f : α → M)
(g : α → N) :
function.support (λ (x : α), (f x, g x)) = function.support f ∪ function.support g
theorem
function.mul_support_prod_mk
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_one M]
[has_one N]
(f : α → M)
(g : α → N) :
function.mul_support (λ (x : α), (f x, g x)) = function.mul_support f ∪ function.mul_support g
theorem
function.mul_support_prod_mk'
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_one M]
[has_one N]
(f : α → M × N) :
function.mul_support f = function.mul_support (λ (x : α), (f x).fst) ∪ function.mul_support (λ (x : α), (f x).snd)
theorem
function.support_prod_mk'
{α : Type u_1}
{M : Type u_5}
{N : Type u_6}
[has_zero M]
[has_zero N]
(f : α → M × N) :
function.support f = function.support (λ (x : α), (f x).fst) ∪ function.support (λ (x : α), (f x).snd)
theorem
function.mul_support_along_fiber_subset
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_one M]
(f : α × β → M)
(a : α) :
function.mul_support (λ (b : β), f (a, b)) ⊆ prod.snd '' function.mul_support f
theorem
function.support_along_fiber_subset
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α × β → M)
(a : α) :
function.support (λ (b : β), f (a, b)) ⊆ prod.snd '' function.support f
@[simp]
theorem
function.support_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α × β → M)
(a : α)
(h : (function.support f).finite) :
(function.support (λ (b : β), f (a, b))).finite
@[simp]
theorem
function.mul_support_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_one M]
(f : α × β → M)
(a : α)
(h : (function.mul_support f).finite) :
(function.mul_support (λ (b : β), f (a, b))).finite
theorem
function.support_add
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(f g : α → M) :
function.support (λ (x : α), f x + g x) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_mul
{α : Type u_1}
{M : Type u_5}
[mul_one_class M]
(f g : α → M) :
function.mul_support (λ (x : α), (f x) * g x) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_nsmul
{α : Type u_1}
{M : Type u_5}
[add_monoid M]
(f : α → M)
(n : ℕ) :
function.support (λ (x : α), n • f x) ⊆ function.support f
theorem
function.mul_support_pow
{α : Type u_1}
{M : Type u_5}
[monoid M]
(f : α → M)
(n : ℕ) :
function.mul_support (λ (x : α), f x ^ n) ⊆ function.mul_support f
@[simp]
theorem
function.mul_support_inv
{α : Type u_1}
{G : Type u_10}
[group G]
(f : α → G) :
function.mul_support (λ (x : α), (f x)⁻¹) = function.mul_support f
@[simp]
theorem
function.support_neg
{α : Type u_1}
{G : Type u_10}
[add_group G]
(f : α → G) :
function.support (λ (x : α), -f x) = function.support f
@[simp]
@[simp]
@[simp]
theorem
function.mul_support_inv₀
{α : Type u_1}
{G₀ : Type u_12}
[group_with_zero G₀]
(f : α → G₀) :
function.mul_support (λ (x : α), (f x)⁻¹) = function.mul_support f
theorem
function.mul_support_mul_inv
{α : Type u_1}
{G : Type u_10}
[group G]
(f g : α → G) :
function.mul_support (λ (x : α), (f x) * (g x)⁻¹) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_add_neg
{α : Type u_1}
{G : Type u_10}
[add_group G]
(f g : α → G) :
function.support (λ (x : α), f x + -g x) ⊆ function.support f ∪ function.support g
theorem
function.support_sub
{α : Type u_1}
{G : Type u_10}
[add_group G]
(f g : α → G) :
function.support (λ (x : α), f x - g x) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_group_div
{α : Type u_1}
{G : Type u_10}
[group G]
(f g : α → G) :
function.mul_support (λ (x : α), f x / g x) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.mul_support_div
{α : Type u_1}
{G₀ : Type u_12}
[group_with_zero G₀]
(f g : α → G₀) :
function.mul_support (λ (x : α), f x / g x) ⊆ function.mul_support f ∪ function.mul_support g
@[simp]
theorem
function.support_mul
{α : Type u_1}
{R : Type u_8}
[mul_zero_class R]
[no_zero_divisors R]
(f g : α → R) :
function.support (λ (x : α), (f x) * g x) = function.support f ∩ function.support g
@[simp]
theorem
function.support_mul_subset_left
{α : Type u_1}
{R : Type u_8}
[mul_zero_class R]
(f g : α → R) :
function.support (λ (x : α), (f x) * g x) ⊆ function.support f
@[simp]
theorem
function.support_mul_subset_right
{α : Type u_1}
{R : Type u_8}
[mul_zero_class R]
(f g : α → R) :
function.support (λ (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}
[add_monoid A]
[monoid B]
[distrib_mul_action B A]
(b : B)
(f : α → A) :
function.support (b • f) ⊆ function.support f
theorem
function.support_smul_subset_left
{α : Type u_1}
{M : Type u_5}
{R : Type u_8}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : α → R)
(g : α → M) :
function.support (f • g) ⊆ function.support f
theorem
function.support_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_8}
[semiring R]
[add_comm_monoid M]
[module R M]
[no_zero_smul_divisors R M]
(f : α → R)
(g : α → M) :
function.support (f • g) = function.support f ∩ function.support g
theorem
function.support_const_smul_of_ne_zero
{α : Type u_1}
{M : Type u_5}
{R : Type u_8}
[semiring R]
[add_comm_monoid M]
[module R M]
[no_zero_smul_divisors 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}
[group_with_zero G₀]
(f : α → G₀) :
function.support (λ (x : α), (f x)⁻¹) = function.support f
@[simp]
theorem
function.support_div
{α : Type u_1}
{G₀ : Type u_12}
[group_with_zero G₀]
(f g : α → G₀) :
function.support (λ (x : α), f x / g x) = function.support f ∩ function.support g
theorem
function.mul_support_prod
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[comm_monoid M]
(s : finset α)
(f : α → β → M) :
function.mul_support (λ (x : β), ∏ (i : α) in s, f i x) ⊆ ⋃ (i : α) (H : i ∈ s), function.mul_support (f i)
theorem
function.support_sum
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(s : finset α)
(f : α → β → M) :
function.support (λ (x : β), ∑ (i : α) in s, f i x) ⊆ ⋃ (i : α) (H : i ∈ s), function.support (f i)
theorem
function.support_prod_subset
{α : Type u_1}
{β : Type u_2}
{A : Type u_3}
[comm_monoid_with_zero A]
(s : finset α)
(f : α → β → A) :
function.support (λ (x : β), ∏ (i : α) in s, f i x) ⊆ ⋂ (i : α) (H : i ∈ s), function.support (f i)
theorem
function.support_prod
{α : Type u_1}
{β : Type u_2}
{A : Type u_3}
[comm_monoid_with_zero A]
[no_zero_divisors A]
[nontrivial A]
(s : finset α)
(f : α → β → A) :
function.support (λ (x : β), ∏ (i : α) in s, f i x) = ⋂ (i : α) (H : i ∈ s), function.support (f i)
theorem
function.mul_support_one_add
{α : Type u_1}
{R : Type u_8}
[has_one R]
[add_left_cancel_monoid R]
(f : α → R) :
function.mul_support (λ (x : α), 1 + f x) = function.support f
theorem
function.mul_support_one_add'
{α : Type u_1}
{R : Type u_8}
[has_one R]
[add_left_cancel_monoid R]
(f : α → R) :
function.mul_support (1 + f) = function.support f
theorem
function.mul_support_add_one
{α : Type u_1}
{R : Type u_8}
[has_one R]
[add_right_cancel_monoid R]
(f : α → R) :
function.mul_support (λ (x : α), f x + 1) = function.support f
theorem
function.mul_support_add_one'
{α : Type u_1}
{R : Type u_8}
[has_one R]
[add_right_cancel_monoid R]
(f : α → R) :
function.mul_support (f + 1) = function.support f
theorem
function.mul_support_one_sub'
{α : Type u_1}
{R : Type u_8}
[has_one R]
[add_group R]
(f : α → R) :
function.mul_support (1 - f) = function.support f
theorem
function.mul_support_one_sub
{α : Type u_1}
{R : Type u_8}
[has_one R]
[add_group R]
(f : α → R) :
function.mul_support (λ (x : α), 1 - f x) = function.support f
theorem
set.image_inter_mul_support_eq
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[has_one M]
{f : α → M}
{s : set β}
{g : β → α} :
g '' s ∩ function.mul_support f = g '' (s ∩ function.mul_support (f ∘ g))
theorem
set.image_inter_support_eq
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[has_zero M]
{f : α → M}
{s : set β}
{g : β → α} :
g '' s ∩ function.support f = g '' (s ∩ function.support (f ∘ g))
theorem
pi.support_single_zero
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_zero B]
{a : A} :
function.support (pi.single a 0) = ∅
@[simp]
theorem
pi.support_single_of_ne
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_zero B]
{a : A}
{b : B}
(h : b ≠ 0) :
function.support (pi.single a b) = {a}
theorem
pi.support_single
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_zero B]
{a : A}
{b : B}
[decidable_eq B] :
theorem
pi.support_single_subset
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_zero B]
{a : A}
{b : B} :
function.support (pi.single a b) ⊆ {a}
theorem
pi.support_single_disjoint
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_zero B]
{b b' : B}
(hb : b ≠ 0)
(hb' : b' ≠ 0)
{i j : A} :
disjoint (function.support (pi.single i b)) (function.support (pi.single j b')) ↔ i ≠ j