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.mulSupport f = {x | f x ≠ 1}
.
mulSupport
of a function is the set of points x
such that f x ≠ 1
.
Instances For
@[deprecated Function.notMem_support (since := "2025-05-24")]
Alias of Function.notMem_support
.
@[deprecated Function.notMem_mulSupport (since := "2025-05-24")]
Alias of Function.notMem_mulSupport
.
@[simp]
theorem
Function.mulSupport_subset_iff'
{ι : Type u_1}
{M : Type u_3}
[One M]
{f : ι → M}
{s : Set ι}
:
theorem
Function.mulSupport_update_of_ne_one
{ι : Type u_1}
{M : Type u_3}
[One M]
[DecidableEq ι]
(f : ι → M)
(x : ι)
{y : M}
(hy : y ≠ 1)
:
theorem
Function.mulSupport_update_one
{ι : Type u_1}
{M : Type u_3}
[One M]
[DecidableEq ι]
(f : ι → M)
(x : ι)
:
theorem
Function.mulSupport_update_eq_ite
{ι : Type u_1}
{M : Type u_3}
[One M]
[DecidableEq ι]
[DecidableEq M]
(f : ι → M)
(x : ι)
(y : M)
:
theorem
Function.mulSupport_extend_one_subset
{ι : Type u_1}
{κ : Type u_2}
{N : Type u_4}
[One N]
{f : ι → κ}
{g : ι → N}
:
theorem
Function.mulSupport_disjoint_iff
{ι : Type u_1}
{M : Type u_3}
[One M]
{f : ι → M}
{s : Set ι}
:
theorem
Function.disjoint_mulSupport_iff
{ι : Type u_1}
{M : Type u_3}
[One M]
{f : ι → M}
{s : Set ι}
:
@[simp]
@[simp]
theorem
Function.range_subset_insert_image_mulSupport
{ι : Type u_1}
{M : Type u_3}
[One M]
(f : ι → M)
:
@[simp]
@[simp]
@[deprecated Function.support_zero (since := "2025-07-31")]
Alias of Function.support_zero
.
@[deprecated Function.mulSupport_one (since := "2025-07-31")]
Alias of Function.mulSupport_one
.
theorem
Function.mulSupport_comp_eq_preimage
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_3}
[One M]
(g : κ → M)
(f : ι → κ)
:
@[deprecated Function.mulSupport_prodMk (since := "2025-07-31")]
theorem
Function.mulSupport_prod_mk
{ι : Type u_1}
{M : Type u_3}
{N : Type u_4}
[One M]
[One N]
(f : ι → M)
(g : ι → N)
:
Alias of Function.mulSupport_prodMk
.
@[deprecated Function.mulSupport_prodMk' (since := "2025-07-31")]
theorem
Function.mulSupport_prod_mk'
{ι : Type u_1}
{M : Type u_3}
{N : Type u_4}
[One M]
[One N]
(f : ι → M × N)
:
Alias of Function.mulSupport_prodMk'
.
@[deprecated Function.mulSupport_fun_curry (since := "2025-07-31")]
theorem
Function.mulSupport_curry'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_3}
[One M]
(f : ι × κ → M)
:
Alias of Function.mulSupport_fun_curry
.
theorem
Pi.mulSupport_mulSingle_subset
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[One M]
{i : ι}
{a : M}
:
theorem
Pi.support_single_subset
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[Zero M]
{i : ι}
{a : M}
:
@[simp]
theorem
Pi.mulSupport_mulSingle_of_ne
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[One M]
{i : ι}
{a : M}
(h : a ≠ 1)
:
@[simp]
theorem
Pi.support_single_of_ne
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[Zero M]
{i : ι}
{a : M}
(h : a ≠ 0)
:
theorem
Pi.mulSupport_mulSingle
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[One M]
{i : ι}
{a : M}
[DecidableEq M]
:
theorem
Pi.support_single
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[Zero M]
{i : ι}
{a : M}
[DecidableEq M]
:
theorem
Pi.mulSupport_mulSingle_disjoint
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[One M]
{i j : ι}
{a b : M}
(ha : a ≠ 1)
(hb : b ≠ 1)
:
theorem
Pi.support_single_disjoint
{ι : Type u_1}
{M : Type u_3}
[DecidableEq ι]
[Zero M]
{i j : ι}
{a b : M}
(ha : a ≠ 0)
(hb : b ≠ 0)
: