mathlib documentation

data.support

Support of a function

In this file we define function.support f = {x | f x ≠ 0} and prove its basic properties.

def function.support {α : Type u} {A : Type x} [has_zero A] :
(α → A)set α

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

Equations
theorem function.nmem_support {α : Type u} {A : Type x} [has_zero A] {f : α → A} {x : α} :

theorem function.mem_support {α : Type u} {A : Type x} [has_zero A] {f : α → A} {x : α} :

theorem function.support_subset_iff {α : Type u} {A : Type x} [has_zero A] {f : α → A} {s : set α} :
function.support f s ∀ (x : α), f x 0x s

theorem function.support_subset_iff' {α : Type u} {A : Type x} [has_zero A] {f : α → A} {s : set α} :
function.support f s ∀ (x : α), x sf x = 0

@[simp]
theorem function.support_eq_empty_iff {α : Type u} {A : Type x} [has_zero A] {f : α → A} :

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) :

@[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) :

@[simp]
theorem function.support_mul {α : Type u} {A : Type x} [mul_zero_class A] [no_zero_divisors A] (f g : α → A) :

@[simp]
theorem function.support_inv {α : Type u} {A : Type x} [division_ring A] (f : α → A) :

@[simp]
theorem function.support_div {α : Type u} {A : Type x} [division_ring A] (f g : α → A) :

theorem function.support_sup {α : Type u} {A : Type x} [has_zero A] [semilattice_sup A] (f g : α → A) :

theorem function.support_inf {α : Type u} {A : Type x} [has_zero A] [semilattice_inf A] (f g : α → A) :

theorem function.support_max {α : Type u} {A : Type x} [has_zero A] [linear_order A] (f g : α → A) :

theorem function.support_min {α : Type u} {A : Type x} [has_zero A] [linear_order A] (f g : α → A) :

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 : β), ∑ (i : α) in s, 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 : β), ∏ (i : α) in s, 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 : β), ∏ (i : α) in s, 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) :

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 = 0x = 0) (f : α → A) :

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) :

theorem function.support_prod_mk {α : Type u} {A : Type x} {B : Type y} [has_zero A] [has_zero B] (f : α → A) (g : α → B) :