HepLean Documentation

Mathlib.Algebra.GroupWithZero.Indicator

Indicator functions and support of a function in groups with zero #

source
theorem Set.indicator_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (g : ι → M₀) :
(s.indicator fun (i : ι) => f i * g i) = fun (i : ι) => s.indicator f i * s.indicator g i
source
theorem Set.indicator_mul_left {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] {i : ι} (s : Set ι) (f : ι → M₀) (g : ι → M₀) :
s.indicator (fun (j : ι) => f j * g j) i = s.indicator f i * g i
source
theorem Set.indicator_mul_right {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] {i : ι} (s : Set ι) (f : ι → M₀) (g : ι → M₀) :
s.indicator (fun (j : ι) => f j * g j) i = f i * s.indicator g i
source
theorem Set.indicator_mul_const {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
s.indicator (fun (x : ι) => f x * a) i = s.indicator f i * a
source
theorem Set.indicator_const_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
s.indicator (fun (x : ι) => a * f x) i = a * s.indicator f i
source
theorem Set.inter_indicator_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] {s : Set ι} {t : Set ι} (f : ι → M₀) (g : ι → M₀) (i : ι) :
(s ∩ t).indicator (fun (j : ι) => f j * g j) i = s.indicator f i * t.indicator g i
source
theorem Set.inter_indicator_one {ι : Type u_1} {M₀ : Type u_4} [MulZeroOneClass M₀] {s : Set ι} {t : Set ι} :
(s ∩ t).indicator 1 = s.indicator 1 * t.indicator 1
source
theorem Set.indicator_prod_one {ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [MulZeroOneClass M₀] {s : Set ι} {i : ι} {t : Set κ} {j : κ} :
(s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j
source
theorem Set.indicator_eq_zero_iff_not_mem {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀] :
s.indicator 1 i = 0 ↔ i ∉ s
source
theorem Set.indicator_eq_one_iff_mem {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀] :
s.indicator 1 i = 1 ↔ i ∈ s
source
theorem Set.indicator_one_inj {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s : Set ι} {t : Set ι} [Nontrivial M₀] (h : s.indicator 1 = t.indicator 1) :
s = t
source
@[simp]
theorem Function.support_one {ι : Type u_1} (R : Type u_5) [Zero R] [One R] [NeZero 1] :
Function.support 1 = Set.univ
source
@[simp]
theorem Function.mulSupport_zero {ι : Type u_1} (R : Type u_5) [Zero R] [One R] [NeZero 1] :
Function.mulSupport 0 = Set.univ
source
theorem Function.support_mul_subset_left {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (f : ι → M₀) (g : ι → M₀) :
(Function.support fun (x : ι) => f x * g x) ⊆ Function.support f
source
theorem Function.support_mul_subset_right {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (f : ι → M₀) (g : ι → M₀) :
(Function.support fun (x : ι) => f x * g x) ⊆ Function.support g
source
@[simp]
theorem Function.support_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f : ι → M₀) (g : ι → M₀) :
(Function.support fun (x : ι) => f x * g x) = Function.support f ∩ Function.support g
source
@[simp]
theorem Function.support_mul' {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f : ι → M₀) (g : ι → M₀) :
Function.support (f * g) = Function.support f ∩ Function.support g
source
@[simp]
theorem Function.support_pow {ι : Type u_1} {M₀ : Type u_4} [MonoidWithZero M₀] [NoZeroDivisors M₀] {n : ℕ} (f : ι → M₀) (hn : n ≠ 0) :
(Function.support fun (a : ι) => f a ^ n) = Function.support f
source
@[simp]
theorem Function.support_pow' {ι : Type u_1} {M₀ : Type u_4} [MonoidWithZero M₀] [NoZeroDivisors M₀] {n : ℕ} (f : ι → M₀) (hn : n ≠ 0) :
Function.support (f ^ n) = Function.support f
source
@[simp]
theorem Function.support_inv {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ι → G₀) :
(Function.support fun (a : ι) => (f a)⁻¹) = Function.support f
source
@[simp]
theorem Function.support_inv' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ι → G₀) :
Function.support f⁻¹ = Function.support f
source
@[simp]
theorem Function.support_div {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ι → G₀) (g : ι → G₀) :
(Function.support fun (a : ι) => f a / g a) = Function.support f ∩ Function.support g
source
@[simp]
theorem Function.support_div' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ι → G₀) (g : ι → G₀) :
Function.support (f / g) = Function.support f ∩ Function.support g
source
theorem Function.mulSupport_one_add {ι : Type u_1} {R : Type u_5} [One R] [AddLeftCancelMonoid R] (f : ι → R) :
(Function.mulSupport fun (x : ι) => 1 + f x) = Function.support f
source
theorem Function.mulSupport_one_add' {ι : Type u_1} {R : Type u_5} [One R] [AddLeftCancelMonoid R] (f : ι → R) :
Function.mulSupport (1 + f) = Function.support f
source
theorem Function.mulSupport_add_one {ι : Type u_1} {R : Type u_5} [One R] [AddRightCancelMonoid R] (f : ι → R) :
(Function.mulSupport fun (x : ι) => f x + 1) = Function.support f
source
theorem Function.mulSupport_add_one' {ι : Type u_1} {R : Type u_5} [One R] [AddRightCancelMonoid R] (f : ι → R) :
Function.mulSupport (f + 1) = Function.support f
source
theorem Function.mulSupport_one_sub' {ι : Type u_1} {R : Type u_5} [One R] [AddGroup R] (f : ι → R) :
Function.mulSupport (1 - f) = Function.support f
source
theorem Function.mulSupport_one_sub {ι : Type u_1} {R : Type u_5} [One R] [AddGroup R] (f : ι → R) :
(Function.mulSupport fun (x : ι) => 1 - f x) = Function.support f