Support of a function

In this file we prove basic properties of Function.support f = {x | f x ≠ 0}, and similarly for Function.mulSupport f = {x | f x ≠ 1}.

theorem Function.mulSupport_mul {α : Type u_1} {M : Type u_2} [MulOneClass M] (f g : α → M) : (mulSupport fun (x : α) => f x * g x) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_add {α : Type u_1} {M : Type u_2} [AddZeroClass M] (f g : α → M) : (support fun (x : α) => f x + g x) ⊆ support f ∪ support g

theorem Function.mulSupport_pow {α : Type u_1} {M : Type u_2} [Monoid M] (f : α → M) (n : ℕ) : (mulSupport fun (x : α) => f x ^ n) ⊆ mulSupport f

theorem Function.support_nsmul {α : Type u_1} {M : Type u_2} [AddMonoid M] (f : α → M) (n : ℕ) : (support fun (x : α) => n • f x) ⊆ support f

@[simp]

theorem Function.mulSupport_fun_inv {α : Type u_1} {G : Type u_3} [DivisionMonoid G] (f : α → G) : (mulSupport fun (x : α) => (f x)⁻¹) = mulSupport f

@[simp]

theorem Function.support_fun_neg {α : Type u_1} {G : Type u_3} [SubtractionMonoid G] (f : α → G) : (support fun (x : α) => -f x) = support f

@[simp]

theorem Function.mulSupport_inv {α : Type u_1} {G : Type u_3} [DivisionMonoid G] (f : α → G) : mulSupport f⁻¹ = mulSupport f

@[simp]

theorem Function.support_neg {α : Type u_1} {G : Type u_3} [SubtractionMonoid G] (f : α → G) : support (-f) = support f

@[deprecated Function.support_neg (since := "2025-07-31")]

theorem Function.support_neg' {α : Type u_1} {G : Type u_3} [SubtractionMonoid G] (f : α → G) : support (-f) = support f

Alias of Function.support_neg.

@[deprecated Function.mulSupport_inv (since := "2025-07-31")]

theorem Function.mulSupport_inv' {α : Type u_1} {G : Type u_3} [DivisionMonoid G] (f : α → G) : mulSupport f⁻¹ = mulSupport f

Alias of Function.mulSupport_inv.

theorem Function.mulSupport_mul_inv {α : Type u_1} {G : Type u_3} [DivisionMonoid G] (f g : α → G) : (mulSupport fun (x : α) => f x * (g x)⁻¹) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_add_neg {α : Type u_1} {G : Type u_3} [SubtractionMonoid G] (f g : α → G) : (support fun (x : α) => f x + -g x) ⊆ support f ∪ support g

theorem Function.mulSupport_div {α : Type u_1} {G : Type u_3} [DivisionMonoid G] (f g : α → G) : (mulSupport fun (x : α) => f x / g x) ⊆ mulSupport f ∪ mulSupport g

theorem Function.support_sub {α : Type u_1} {G : Type u_3} [SubtractionMonoid G] (f g : α → G) : (support fun (x : α) => f x - g x) ⊆ support f ∪ support g