data.support

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

def function.support {α : Type u_1} {A : Type u_3} [has_zero A] (f : α → A) :
set α

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

Equations
• = {x : α | f x 0}
def function.mul_support {α : Type u_1} {M : Type u_5} [has_one M] (f : α → M) :
set α

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

Equations
• = {x : α | f x 1}
theorem function.nmem_mul_support {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} {x : α} :
f x = 1
theorem function.nmem_support {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {x : α} :
f x = 0
theorem function.compl_mul_support {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} :
= {x : α | f x = 1}
theorem function.compl_support {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} :
= {x : α | f x = 0}
@[simp]
theorem function.mem_mul_support {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} {x : α} :
f x 1
@[simp]
theorem function.mem_support {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {x : α} :
f x 0
@[simp]
theorem function.support_subset_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {s : set α} :
∀ (x : α), f x 0x s
@[simp]
theorem function.mul_support_subset_iff {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} {s : set α} :
∀ (x : α), f x 1x s
theorem function.support_subset_iff' {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {s : set α} :
∀ (x : α), x sf x = 0
theorem function.mul_support_subset_iff' {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} {s : set α} :
∀ (x : α), x sf x = 1
@[simp]
theorem function.mul_support_eq_empty_iff {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} :
f = 1
@[simp]
theorem function.support_eq_empty_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} :
f = 0
@[simp]
theorem function.support_zero' {α : Type u_1} {M : Type u_5} [has_zero M] :
@[simp]
theorem function.mul_support_one' {α : Type u_1} {M : Type u_5} [has_one M] :
@[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_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))
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))
theorem function.support_sup {α : Type u_1} {M : Type u_5} [has_zero M] (f g : α → M) :
function.support (λ (x : α), f x g x)
theorem function.mul_support_sup {α : Type u_1} {M : Type u_5} [has_one M] (f g : α → M) :
function.mul_support (λ (x : α), f x g x)
theorem function.support_inf {α : Type u_1} {M : Type u_5} [has_zero M] (f g : α → M) :
function.support (λ (x : α), f x g x)
theorem function.mul_support_inf {α : Type u_1} {M : Type u_5} [has_one M] (f g : α → M) :
function.mul_support (λ (x : α), f x g x)
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))
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))
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))
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))
theorem function.mul_support_supr {α : Type u_1} {M : Type u_5} {ι : Sort u_13} [has_one 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] [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] [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] [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) :
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) :
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 = 1x = 1) (f : α → M) :
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 = 0x = 0) (f : α → M) :
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) :
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) :
theorem function.support_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (g : β → M) (f : α → β) :
theorem function.mul_support_comp_eq_preimage {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_one M] (g : β → M) (f : α → β) :
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)) =
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)) =
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 (λ (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 (λ (x : α), (f x).fst) function.support (λ (x : α), (f x).snd)
theorem function.support_add {α : Type u_1} {M : Type u_5} [add_monoid M] (f g : α → M) :
function.support (λ (x : α), f x + g x)
theorem function.mul_support_mul {α : Type u_1} {M : Type u_5} [monoid M] (f g : α → M) :
function.mul_support (λ (x : α), (f x) * g x)
@[simp]
theorem function.mul_support_inv {α : Type u_1} {G : Type u_10} [group G] (f : α → G) :
function.mul_support (λ (x : α), (f x)⁻¹) =
@[simp]
theorem function.support_neg {α : Type u_1} {G : Type u_10} [add_group G] (f : α → G) :
function.support (λ (x : α), -f x) =
@[simp]
theorem function.mul_support_inv'' {α : Type u_1} {G : Type u_10} [group G] (f : α → G) :
@[simp]
theorem function.support_neg' {α : Type u_1} {G : Type u_10} [add_group G] (f : α → G) :
@[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)⁻¹) =
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)⁻¹)
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)
theorem function.support_sub {α : Type u_1} {G : Type u_10} [add_group G] (f g : α → G) :
function.support (λ (x : α), f x - g x)
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)
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)
@[simp]
theorem function.support_mul {α : Type u_1} {R : Type u_8} (f g : α → R) :
function.support (λ (x : α), (f x) * g x) =
theorem function.support_smul_subset_right {α : Type u_1} {A : Type u_3} {B : Type u_4} [add_monoid A] [monoid B] [ A] (b : B) (f : α → A) :
theorem function.support_smul_subset_left {α : Type u_1} {M : Type u_5} {R : Type u_8} [semiring R] [ M] (f : α → R) (g : α → M) :
theorem function.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_8} [semiring R] [ M] (f : α → R) (g : α → M) :
@[simp]
theorem function.support_inv {α : Type u_1} {G₀ : Type u_12} [group_with_zero G₀] (f : α → G₀) :
function.support (λ (x : α), (f x)⁻¹) =
@[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) =
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} (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} (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} [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] (f : α → R) :
function.mul_support (λ (x : α), 1 + f x) =
theorem function.mul_support_one_add' {α : Type u_1} {R : Type u_8} [has_one R] (f : α → R) :
theorem function.mul_support_add_one {α : Type u_1} {R : Type u_8} [has_one R] (f : α → R) :
function.mul_support (λ (x : α), f x + 1) =
theorem function.mul_support_add_one' {α : Type u_1} {R : Type u_8} [has_one R] (f : α → R) :
theorem function.mul_support_one_sub' {α : Type u_1} {R : Type u_8} [has_one R] [add_group R] (f : α → R) :
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) =
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 : β → α} :
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 = 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} :
@[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) :
= {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] :
= ite (b = 0) {a}
theorem pi.support_single_subset {A : Type u_1} {B : Type u_2} [decidable_eq A] [has_zero B] {a : A} {b : 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} :