algebra.support

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

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.support_eq_preimage {α : Type u_1} {M : Type u_5} [has_zero M] (f : α M) :
= f ⁻¹' {0}
theorem function.mul_support_eq_preimage {α : Type u_1} {M : Type u_5} [has_one M] (f : α M) :
= f ⁻¹' {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 0 x 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 1 x s
theorem function.support_subset_iff' {α : Type u_1} {M : Type u_5} [has_zero M] {f : α M} {s : set α} :
(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 α} :
(x : α), x s f x = 1
theorem function.support_eq_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α M} {s : set α} :
( (x : α), x s f x 0) (x : α), x s f x = 0
theorem function.mul_support_eq_iff {α : Type u_1} {M : Type u_5} [has_one M] {f : α M} {s : set α} :
( (x : α), x s f x 1) (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 α} :
s 0 s
theorem function.mul_support_disjoint_iff {α : Type u_1} {M : Type u_5} [has_one M] {f : α M} {s : set α} :
1 s
theorem function.disjoint_support_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α M} {s : set α} :
0 s
theorem function.disjoint_mul_support_iff {α : Type u_1} {M : Type u_5} [has_one M] {f : α M} {s : set α} :
1 s
@[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_nonempty_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α M} :
f 0
@[simp]
theorem function.mul_support_nonempty_iff {α : Type u_1} {M : Type u_5} [has_one M] {f : α M} :
f 1
theorem function.range_subset_insert_image_support {α : Type u_1} {M : Type u_5} [has_zero M] (f : α M) :
(f ''
theorem function.range_subset_insert_image_mul_support {α : Type u_1} {M : Type u_5} [has_one M] (f : α M) :
@[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_const {α : Type u_1} {M : Type u_5} [has_one M] {c : M} (hc : c 1) :
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))
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 : α), linear_order.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 : α), linear_order.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 : α), linear_order.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 : α), linear_order.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 = 1 x = 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 = 0 x = 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.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))
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))
@[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 : .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 : .finite) :
(function.mul_support (λ (b : β), f (a, b))).finite
theorem function.support_add {α : Type u_1} {M : Type u_5} (f g : α M) :
function.support (λ (x : α), f x + g x)
theorem function.mul_support_mul {α : Type u_1} {M : Type u_5} (f g : α M) :
function.mul_support (λ (x : α), f x * g x)
theorem function.support_nsmul {α : Type u_1} {M : Type u_5} [add_monoid M] (f : α M) (n : ) :
function.support (λ (x : α), n f x)
theorem function.mul_support_pow {α : Type u_1} {M : Type u_5} [monoid M] (f : α M) (n : ) :
function.mul_support (λ (x : α), f x ^ n)
@[simp]
theorem function.mul_support_inv {α : Type u_1} {G : Type u_10} (f : α G) :
function.mul_support (λ (x : α), (f x)⁻¹) =
@[simp]
theorem function.support_neg {α : Type u_1} {G : Type u_10} (f : α G) :
function.support (λ (x : α), -f x) =
@[simp]
theorem function.mul_support_inv' {α : Type u_1} {G : Type u_10} (f : α G) :
@[simp]
theorem function.support_neg' {α : Type u_1} {G : Type u_10} (f : α G) :
theorem function.mul_support_mul_inv {α : Type u_1} {G : Type u_10} (f g : α G) :
function.mul_support (λ (x : α), f x * (g x)⁻¹)
theorem function.support_add_neg {α : Type u_1} {G : Type u_10} (f g : α G) :
function.support (λ (x : α), f x + -g x)
theorem function.mul_support_div {α : Type u_1} {G : Type u_10} (f g : α G) :
function.mul_support (λ (x : α), f x / g x)
theorem function.support_sub {α : Type u_1} {G : Type u_10} (f g : α G) :
function.support (λ (x : α), f x - g x)
@[simp]
theorem function.support_one {α : Type u_1} (R : Type u_8) [has_zero R] [has_one R] [ne_zero 1] :
@[simp]
theorem function.mul_support_zero {α : Type u_1} (R : Type u_8) [has_zero R] [has_one R] [ne_zero 1] :
theorem function.support_nat_cast {α : Type u_1} {R : Type u_8} [char_zero R] {n : } (hn : n 0) :
theorem function.mul_support_nat_cast {α : Type u_1} {R : Type u_8} [char_zero R] {n : } (hn : n 1) :
theorem function.support_int_cast {α : Type u_1} {R : Type u_8} [char_zero R] {n : } (hn : n 0) :
theorem function.mul_support_int_cast {α : Type u_1} {R : Type u_8} [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] [ M] (f : α R) (g : α M) :
@[simp]
theorem function.support_mul {α : Type u_1} {R : Type u_8} (f g : α R) :
function.support (λ (x : α), f x * g x) =
@[simp]
theorem function.support_mul_subset_left {α : Type u_1} {R : Type u_8} (f g : α R) :
function.support (λ (x : α), f x * g x)
@[simp]
theorem function.support_mul_subset_right {α : 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} {β : Type u_2} {M : Type u_5} [has_zero M] [has_zero β] [ β] (f : α M) (g : α β) :
theorem function.support_const_smul_of_ne_zero {α : Type u_1} {M : Type u_5} {R : Type u_8} [semiring R] [ M] (c : R) (g : α M) (hc : c 0) :
@[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 : β), 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} (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} (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} [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] (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_subset {A : Type u_1} {B : Type u_2} [decidable_eq A] [has_zero B] {a : A} {b : 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} :
{a}
theorem pi.mul_support_mul_single_one {A : Type u_1} {B : Type u_2} [decidable_eq A] [has_one B] {a : A} :
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}
@[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) :
= {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] :
= 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] :
= ite (b = 0) {a}
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} :
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} :