Support of a function
In this file we define function.support f = {x | f x ≠ 0} and prove its basic properties.
support of a function is the set of points x such that f x ≠ 0.
Equations
- function.support f = {x : α | f x ≠ 0}
theorem
function.nmem_support
{α : Type u}
{A : Type x}
[has_zero A]
{f : α → A}
{x : α} :
x ∉ function.support f ↔ f x = 0
theorem
function.mem_support
{α : Type u}
{A : Type x}
[has_zero A]
{f : α → A}
{x : α} :
x ∈ function.support f ↔ f x ≠ 0
theorem
function.support_subset_iff
{α : Type u}
{A : Type x}
[has_zero A]
{f : α → A}
{s : set α} :
function.support f ⊆ s ↔ ∀ (x : α), f x ≠ 0 → x ∈ s
theorem
function.support_subset_iff'
{α : Type u}
{A : Type x}
[has_zero A]
{f : α → A}
{s : set α} :
function.support f ⊆ s ↔ ∀ (x : α), x ∉ s → f x = 0
theorem
function.support_binop_subset
{α : Type u}
{A : Type x}
[has_zero A]
(op : A → A → A)
(op0 : op 0 0 = 0)
(f g : α → A) :
function.support (λ (x : α), op (f x) (g x)) ⊆ function.support f ∪ function.support g
theorem
function.support_add
{α : Type u}
{A : Type x}
[add_monoid A]
(f g : α → A) :
function.support (λ (x : α), f x + g x) ⊆ function.support f ∪ function.support g
@[simp]
theorem
function.support_neg
{α : Type u}
{A : Type x}
[add_group A]
(f : α → A) :
function.support (λ (x : α), -f x) = function.support f
theorem
function.support_sub
{α : Type u}
{A : Type x}
[add_group A]
(f g : α → A) :
function.support (λ (x : α), f x - g x) ⊆ function.support f ∪ function.support g
@[simp]
theorem
function.support_mul
{α : Type u}
{A : Type x}
[mul_zero_class A]
[no_zero_divisors A]
(f g : α → A) :
function.support (λ (x : α), f x * g x) = function.support f ∩ function.support g
@[simp]
theorem
function.support_inv
{α : Type u}
{A : Type x}
[division_ring A]
(f : α → A) :
function.support (λ (x : α), (f x)⁻¹) = function.support f
@[simp]
theorem
function.support_div
{α : Type u}
{A : Type x}
[division_ring A]
(f g : α → A) :
function.support (λ (x : α), f x / g x) = function.support f ∩ function.support g
theorem
function.support_sup
{α : Type u}
{A : Type x}
[has_zero A]
[semilattice_sup A]
(f g : α → A) :
function.support (λ (x : α), f x ⊔ g x) ⊆ function.support f ∪ function.support g
theorem
function.support_inf
{α : Type u}
{A : Type x}
[has_zero A]
[semilattice_inf A]
(f g : α → A) :
function.support (λ (x : α), f x ⊓ g x) ⊆ function.support f ∪ function.support g
theorem
function.support_max
{α : Type u}
{A : Type x}
[has_zero A]
[decidable_linear_order A]
(f g : α → A) :
function.support (λ (x : α), max (f x) (g x)) ⊆ function.support f ∪ function.support g
theorem
function.support_min
{α : Type u}
{A : Type x}
[has_zero A]
[decidable_linear_order A]
(f g : α → A) :
function.support (λ (x : α), min (f x) (g x)) ⊆ function.support f ∪ function.support g
theorem
function.support_supr
{α : Type u}
{ι : Sort w}
{A : Type x}
[has_zero A]
[conditionally_complete_lattice A]
[nonempty ι]
(f : ι → α → A) :
function.support (λ (x : α), ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), function.support (f i)
theorem
function.support_infi
{α : Type u}
{ι : Sort w}
{A : Type x}
[has_zero A]
[conditionally_complete_lattice A]
[nonempty ι]
(f : ι → α → A) :
function.support (λ (x : α), ⨅ (i : ι), f i x) ⊆ ⋃ (i : ι), function.support (f i)
theorem
function.support_sum
{α : Type u}
{β : Type v}
{A : Type x}
[add_comm_monoid A]
(s : finset α)
(f : α → β → A) :
function.support (λ (x : β), s.sum (λ (i : α), f i x)) ⊆ ⋃ (i : α) (H : i ∈ s), function.support (f i)
theorem
function.support_prod_subset
{α : Type u}
{β : Type v}
{A : Type x}
[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}
{β : Type v}
{A : Type x}
[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.support_comp_subset
{α : Type u}
{A : Type x}
{B : Type y}
[has_zero A]
[has_zero B]
{g : A → B}
(hg : g 0 = 0)
(f : α → A) :
function.support (g ∘ f) ⊆ function.support f
theorem
function.support_subset_comp
{α : Type u}
{A : Type x}
{B : Type y}
[has_zero A]
[has_zero B]
{g : A → B}
(hg : ∀ {x : A}, g x = 0 → x = 0)
(f : α → A) :
function.support f ⊆ function.support (g ∘ f)
theorem
function.support_comp_eq
{α : Type u}
{A : Type x}
{B : Type y}
[has_zero A]
[has_zero B]
(g : A → B)
(hg : ∀ {x : A}, g x = 0 ↔ x = 0)
(f : α → A) :
function.support (g ∘ f) = function.support f
theorem
function.support_prod_mk
{α : Type u}
{A : Type x}
{B : Type y}
[has_zero A]
[has_zero B]
(f : α → A)
(g : α → B) :
function.support (λ (x : α), (f x, g x)) = function.support f ∪ function.support g