Support of a function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_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
theorem
function.range_subset_insert_image_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α → M) :
set.range f ⊆ has_insert.insert 0 (f '' function.support f)
theorem
function.range_subset_insert_image_mul_support
{α : Type u_1}
{M : Type u_5}
[has_one M]
(f : α → M) :
set.range f ⊆ has_insert.insert 1 (f '' function.mul_support f)
@[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 : α), linear_order.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 : α), linear_order.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 : α), linear_order.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 : α), linear_order.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.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}
[division_monoid 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}
[subtraction_monoid G]
(f : α → G) :
function.support (λ (x : α), -f x) = function.support f
@[simp]
@[simp]
theorem
function.mul_support_mul_inv
{α : Type u_1}
{G : Type u_10}
[division_monoid 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}
[subtraction_monoid G]
(f g : α → G) :
function.support (λ (x : α), f x + -g x) ⊆ function.support f ∪ function.support g
theorem
function.mul_support_div
{α : Type u_1}
{G : Type u_10}
[division_monoid G]
(f g : α → G) :
function.mul_support (λ (x : α), f x / g x) ⊆ function.mul_support f ∪ function.mul_support g
theorem
function.support_sub
{α : Type u_1}
{G : Type u_10}
[subtraction_monoid G]
(f g : α → G) :
function.support (λ (x : α), f x - g x) ⊆ function.support f ∪ function.support g
theorem
function.support_nat_cast
{α : Type u_1}
{R : Type u_8}
[add_monoid_with_one R]
[char_zero R]
{n : ℕ}
(hn : n ≠ 0) :
theorem
function.mul_support_nat_cast
{α : Type u_1}
{R : Type u_8}
[add_monoid_with_one R]
[char_zero R]
{n : ℕ}
(hn : n ≠ 1) :
theorem
function.support_int_cast
{α : Type u_1}
{R : Type u_8}
[add_group_with_one R]
[char_zero R]
{n : ℤ}
(hn : n ≠ 0) :
theorem
function.mul_support_int_cast
{α : Type u_1}
{R : Type u_8}
[add_group_with_one R]
[char_zero R]
{n : ℤ}
(hn : n ≠ 1) :
theorem
function.support_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_8}
[has_zero R]
[has_zero M]
[smul_with_zero R M]
[no_zero_smul_divisors 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}
[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}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
[has_zero β]
[smul_with_zero 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]
[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 : β), s.prod (λ (i : α), 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 : β), s.sum (λ (i : α), 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 : β), s.prod (λ (i : α), 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 : β), s.prod (λ (i : α), 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
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.mul_support_mul_single_subset
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_one B]
{a : A}
{b : B} :
function.mul_support (pi.mul_single a b) ⊆ {a}
theorem
pi.mul_support_mul_single_one
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_one B]
{a : A} :
function.mul_support (pi.mul_single a 1) = ∅
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}
@[simp]
theorem
pi.mul_support_mul_single_of_ne
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_one B]
{a : A}
{b : B}
(h : b ≠ 1) :
function.mul_support (pi.mul_single a b) = {a}
theorem
pi.mul_support_mul_single
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_one B]
{a : A}
{b : B}
[decidable_eq B] :
function.mul_support (pi.mul_single a b) = ite (b = 1) ∅ {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.mul_support_mul_single_disjoint
{A : Type u_1}
{B : Type u_2}
[decidable_eq A]
[has_one B]
{b b' : B}
(hb : b ≠ 1)
(hb' : b' ≠ 1)
{i j : A} :
disjoint (function.mul_support (pi.mul_single i b)) (function.mul_support (pi.mul_single j b')) ↔ i ≠ j
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