mathlib documentation

algebra.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
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
theorem function.support_eq_preimage {α : Type u_1} {M : Type u_5} [has_zero M] (f : α → M) :
theorem function.mul_support_eq_preimage {α : Type u_1} {M : Type u_5} [has_one M] (f : α → M) :
theorem function.nmem_mul_support {α : Type u_1} {M : Type u_5} [has_one M] {f : α → M} {x : α} :
theorem function.nmem_support {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {x : α} :
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 : α} :
@[simp]
theorem function.mem_support {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {x : α} :
@[simp]
theorem function.support_subset_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {s : set α} :
function.support f s ∀ (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 α} :
function.mul_support f s ∀ (x : α), f x 1x s
theorem function.support_subset_iff' {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {s : set α} :
function.support f s ∀ (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 α} :
function.mul_support f s ∀ (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} :
@[simp]
theorem function.support_eq_empty_iff {α : Type u_1} {M : Type u_5} [has_zero 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) :
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) :
theorem function.mul_support_sup {α : Type u_1} {M : Type u_5} [has_one M] [semilattice_sup M] (f g : α → M) :
theorem function.support_inf {α : Type u_1} {M : Type u_5} [has_zero M] [semilattice_inf M] (f g : α → M) :
theorem function.mul_support_inf {α : Type u_1} {M : Type u_5} [has_one M] [semilattice_inf M] (f g : α → M) :
theorem function.mul_support_max {α : Type u_1} {M : Type u_5} [has_one M] [linear_order M] (f g : α → M) :
theorem function.support_max {α : Type u_1} {M : Type u_5} [has_zero M] [linear_order M] (f g : α → M) :
theorem function.mul_support_min {α : Type u_1} {M : Type u_5} [has_one M] [linear_order M] (f g : α → M) :
theorem function.support_min {α : Type u_1} {M : Type u_5} [has_zero M] [linear_order M] (f g : α → M) :
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) :
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) :
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) :
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 : α) :
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_monoid M] (f g : α → M) :
theorem function.mul_support_mul {α : Type u_1} {M : Type u_5} [monoid M] (f g : α → M) :
@[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) :
function.support (λ (x : α), -f x) = function.support f
@[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₀) :
theorem function.mul_support_mul_inv {α : Type u_1} {G : Type u_10} [group G] (f g : α → G) :
theorem function.support_add_neg {α : Type u_1} {G : Type u_10} [add_group G] (f g : α → G) :
theorem function.support_sub {α : Type u_1} {G : Type u_10} [add_group G] (f g : α → G) :
theorem function.mul_support_group_div {α : Type u_1} {G : Type u_10} [group G] (f g : α → G) :
theorem function.mul_support_div {α : Type u_1} {G₀ : Type u_12} [group_with_zero G₀] (f g : α → G₀) :
@[simp]
theorem function.support_mul {α : Type u_1} {R : Type u_8} [mul_zero_class R] [no_zero_divisors R] (f g : α → R) :
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) :
theorem function.support_smul_subset_left {α : Type u_1} {M : Type u_5} {R : Type u_8} [semiring R] [add_comm_monoid M] [module R M] (f : α → R) (g : α → M) :
theorem function.support_smul {α : 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] (f : α → R) (g : α → M) :
@[simp]
theorem function.support_inv {α : Type u_1} {G₀ : Type u_12} [group_with_zero G₀] (f : α → G₀) :
@[simp]
theorem function.support_div {α : Type u_1} {G₀ : Type u_12} [group_with_zero G₀] (f g : α → 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 : β), ∏ (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} [add_comm_monoid M] (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} [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_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 : β), ∏ (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] [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) :
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) :
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) = function.support f
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 : β → α} :
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) :
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.support_single_subset {A : Type u_1} {B : Type u_2} [decidable_eq A] [has_zero B] {a : A} {b : B} :
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} :