Make fun_prop work for finite (mulitplicative) support #
We provide API lemmas for the predicate HasFiniteMulSupport (and its additivized version
HasFiniteSupport) on functions so that fun_prop can prove it for functions that are
built from other functions with finite multiplicative support.
theorem
Function.HasFiniteMulSupport.fun_comp
{α : Type u_1}
{M : Type u_2}
[One M]
{N : Type u_3}
[One N]
{g : M → N}
{f : α → M}
(hf : HasFiniteMulSupport f)
(hg : g 1 = 1)
:
HasFiniteMulSupport fun (a : α) => g (f a)
theorem
Function.HasFiniteSupport.fun_comp
{α : Type u_1}
{M : Type u_2}
[Zero M]
{N : Type u_3}
[Zero N]
{g : M → N}
{f : α → M}
(hf : HasFiniteSupport f)
(hg : g 0 = 0)
:
HasFiniteSupport fun (a : α) => g (f a)
theorem
Function.HasFiniteMulSupport.comp
{α : Type u_1}
{M : Type u_2}
[One M]
{N : Type u_3}
[One N]
{g : M → N}
{f : α → M}
(hf : HasFiniteMulSupport f)
(hg : g 1 = 1)
:
HasFiniteMulSupport (g ∘ f)
theorem
Function.HasFiniteSupport.comp
{α : Type u_1}
{M : Type u_2}
[Zero M]
{N : Type u_3}
[Zero N]
{g : M → N}
{f : α → M}
(hf : HasFiniteSupport f)
(hg : g 0 = 0)
:
HasFiniteSupport (g ∘ f)
theorem
Function.HasFiniteMulSupport.fst
{α : Type u_1}
{M : Type u_2}
[One M]
{M' : Type u_3}
[One M']
{f : α → M × M'}
(hf : HasFiniteMulSupport f)
:
HasFiniteMulSupport fun (a : α) => (f a).1
theorem
Function.HasFiniteSupport.fst
{α : Type u_1}
{M : Type u_2}
[Zero M]
{M' : Type u_3}
[Zero M']
{f : α → M × M'}
(hf : HasFiniteSupport f)
:
HasFiniteSupport fun (a : α) => (f a).1
theorem
Function.HasFiniteMulSupport.snd
{α : Type u_1}
{M : Type u_2}
[One M]
{M' : Type u_3}
[One M']
{f : α → M × M'}
(hf : HasFiniteMulSupport f)
:
HasFiniteMulSupport fun (a : α) => (f a).2
theorem
Function.HasFiniteSupport.snd
{α : Type u_1}
{M : Type u_2}
[Zero M]
{M' : Type u_3}
[Zero M']
{f : α → M × M'}
(hf : HasFiniteSupport f)
:
HasFiniteSupport fun (a : α) => (f a).2
theorem
Function.HasFiniteMulSupport.prodMk
{α : Type u_1}
{M : Type u_2}
[One M]
{M' : Type u_3}
[One M']
{f : α → M}
{g : α → M'}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (a : α) => (f a, g a)
theorem
Function.HasFiniteSupport.sumMk
{α : Type u_1}
{M : Type u_2}
[Zero M]
{M' : Type u_3}
[Zero M']
{f : α → M}
{g : α → M'}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (a : α) => (f a, g a)
theorem
Function.HasFiniteMulSupport.mul
{α : Type u_1}
{M : Type u_3}
[MulOneClass M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport (f * g)
theorem
Function.HasFiniteSupport.add
{α : Type u_1}
{M : Type u_3}
[AddZeroClass M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport (f + g)
theorem
Function.HasFiniteSupport.fun_add
{α : Type u_1}
{M : Type u_3}
[AddZeroClass M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (i : α) => f i + g i
Eta-expanded form of Function.HasFiniteSupport.add
theorem
Function.HasFiniteMulSupport.fun_mul
{α : Type u_1}
{M : Type u_3}
[MulOneClass M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (i : α) => f i * g i
Eta-expanded form of Function.HasFiniteMulSupport.mul
theorem
Function.HasFiniteMulSupport.inv
{α : Type u_1}
{M : Type u_3}
[DivisionMonoid M]
{f : α → M}
(hf : HasFiniteMulSupport f)
:
theorem
Function.HasFiniteSupport.neg
{α : Type u_1}
{M : Type u_3}
[SubtractionMonoid M]
{f : α → M}
(hf : HasFiniteSupport f)
:
theorem
Function.HasFiniteMulSupport.fun_inv
{α : Type u_1}
{M : Type u_3}
[DivisionMonoid M]
{f : α → M}
(hf : HasFiniteMulSupport f)
:
HasFiniteMulSupport fun (i : α) => (f i)⁻¹
Eta-expanded form of Function.HasFiniteMulSupport.inv
theorem
Function.HasFiniteSupport.fun_neg
{α : Type u_1}
{M : Type u_3}
[SubtractionMonoid M]
{f : α → M}
(hf : HasFiniteSupport f)
:
HasFiniteSupport fun (i : α) => -f i
Eta-expanded form of Function.HasFiniteSupport.neg
theorem
Function.HasFiniteMulSupport.prod
{α : Type u_1}
{M : Type u_3}
[CommMonoid M]
{ι : Type u_4}
{f : ι → α → M}
(hf : ∀ (i : ι), HasFiniteMulSupport (f i))
(s : Finset ι)
:
HasFiniteMulSupport fun (a : α) => ∏ i ∈ s, f i a
theorem
Function.HasFiniteSupport.sum
{α : Type u_1}
{M : Type u_3}
[AddCommMonoid M]
{ι : Type u_4}
{f : ι → α → M}
(hf : ∀ (i : ι), HasFiniteSupport (f i))
(s : Finset ι)
:
HasFiniteSupport fun (a : α) => ∑ i ∈ s, f i a
theorem
Function.HasFiniteMulSupport.div
{α : Type u_1}
{M : Type u_3}
[DivisionMonoid M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport (f / g)
theorem
Function.HasFiniteSupport.sub
{α : Type u_1}
{M : Type u_3}
[SubtractionMonoid M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport (f - g)
theorem
Function.HasFiniteMulSupport.fun_div
{α : Type u_1}
{M : Type u_3}
[DivisionMonoid M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (i : α) => f i / g i
Eta-expanded form of Function.HasFiniteMulSupport.div
theorem
Function.HasFiniteSupport.fun_sub
{α : Type u_1}
{M : Type u_3}
[SubtractionMonoid M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (i : α) => f i - g i
Eta-expanded form of Function.HasFiniteSupport.sub
theorem
Function.HasFiniteMulSupport.pow
{α : Type u_1}
{M : Type u_3}
[Monoid M]
{f : α → M}
(hf : HasFiniteMulSupport f)
(n : ℕ)
:
HasFiniteMulSupport (f ^ n)
theorem
Function.HasFiniteSupport.nsmul
{α : Type u_1}
{M : Type u_3}
[AddMonoid M]
{f : α → M}
(hf : HasFiniteSupport f)
(n : ℕ)
:
HasFiniteSupport (n • f)
theorem
Function.HasFiniteMulSupport.fun_pow
{α : Type u_1}
{M : Type u_3}
[Monoid M]
{f : α → M}
(hf : HasFiniteMulSupport f)
(n : ℕ)
:
HasFiniteMulSupport fun (i : α) => f i ^ n
Eta-expanded form of Function.HasFiniteMulSupport.pow
theorem
Function.HasFiniteSupport.fun_nsmul
{α : Type u_1}
{M : Type u_3}
[AddMonoid M]
{f : α → M}
(hf : HasFiniteSupport f)
(n : ℕ)
:
HasFiniteSupport fun (i : α) => n • f i
Eta-expanded form of Function.HasFiniteSupport.nsmul
theorem
Function.HasFiniteMulSupport.zpow
{α : Type u_1}
{M : Type u_3}
[DivisionMonoid M]
{f : α → M}
(hf : HasFiniteMulSupport f)
(n : ℤ)
:
HasFiniteMulSupport (f ^ n)
theorem
Function.HasFiniteSupport.zsmul
{α : Type u_1}
{M : Type u_3}
[SubtractionMonoid M]
{f : α → M}
(hf : HasFiniteSupport f)
(n : ℤ)
:
HasFiniteSupport (n • f)
theorem
Function.HasFiniteSupport.fun_zsmul
{α : Type u_1}
{M : Type u_3}
[SubtractionMonoid M]
{f : α → M}
(hf : HasFiniteSupport f)
(n : ℤ)
:
HasFiniteSupport fun (i : α) => n • f i
Eta-expanded form of Function.HasFiniteSupport.zsmul
theorem
Function.HasFiniteMulSupport.fun_zpow
{α : Type u_1}
{M : Type u_3}
[DivisionMonoid M]
{f : α → M}
(hf : HasFiniteMulSupport f)
(n : ℤ)
:
HasFiniteMulSupport fun (i : α) => f i ^ n
Eta-expanded form of Function.HasFiniteMulSupport.zpow
theorem
Function.HasFiniteMulSupport.max
{α : Type u_1}
{M : Type u_2}
[One M]
[LinearOrder M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (a : α) => Max.max (f a) (g a)
theorem
Function.HasFiniteSupport.max
{α : Type u_1}
{M : Type u_2}
[Zero M]
[LinearOrder M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (a : α) => Max.max (f a) (g a)
theorem
Function.HasFiniteMulSupport.min
{α : Type u_1}
{M : Type u_2}
[One M]
[LinearOrder M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (a : α) => Min.min (f a) (g a)
theorem
Function.HasFiniteSupport.min
{α : Type u_1}
{M : Type u_2}
[Zero M]
[LinearOrder M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (a : α) => Min.min (f a) (g a)
theorem
Function.HasFiniteMulSupport.sup
{α : Type u_1}
{M : Type u_2}
[One M]
[SemilatticeSup M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (a : α) => f a ⊔ g a
theorem
Function.HasFiniteSupport.sup
{α : Type u_1}
{M : Type u_2}
[Zero M]
[SemilatticeSup M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (a : α) => f a ⊔ g a
theorem
Function.HasFiniteMulSupport.inf
{α : Type u_1}
{M : Type u_2}
[One M]
[SemilatticeInf M]
{f g : α → M}
(hf : HasFiniteMulSupport f)
(hg : HasFiniteMulSupport g)
:
HasFiniteMulSupport fun (a : α) => f a ⊓ g a
theorem
Function.HasFiniteSupport.inf
{α : Type u_1}
{M : Type u_2}
[Zero M]
[SemilatticeInf M]
{f g : α → M}
(hf : HasFiniteSupport f)
(hg : HasFiniteSupport g)
:
HasFiniteSupport fun (a : α) => f a ⊓ g a
theorem
Function.HasFiniteMulSupport.iSup
{α : Type u_1}
{M : Type u_2}
[One M]
[ConditionallyCompleteLattice M]
{ι : Sort u_3}
[Nonempty ι]
[Finite ι]
{f : ι → α → M}
(hf : ∀ (i : ι), HasFiniteMulSupport (f i))
:
HasFiniteMulSupport fun (a : α) => ⨆ (i : ι), f i a
theorem
Function.HasFiniteSupport.iSup
{α : Type u_1}
{M : Type u_2}
[Zero M]
[ConditionallyCompleteLattice M]
{ι : Sort u_3}
[Nonempty ι]
[Finite ι]
{f : ι → α → M}
(hf : ∀ (i : ι), HasFiniteSupport (f i))
:
HasFiniteSupport fun (a : α) => ⨆ (i : ι), f i a
theorem
Function.HasFiniteMulSupport.iInf
{α : Type u_1}
{M : Type u_2}
[One M]
[ConditionallyCompleteLattice M]
{ι : Sort u_3}
[Nonempty ι]
[Finite ι]
{f : ι → α → M}
(hf : ∀ (i : ι), HasFiniteMulSupport (f i))
:
HasFiniteMulSupport fun (a : α) => ⨅ (i : ι), f i a
theorem
Function.HasFiniteSupport.iInf
{α : Type u_1}
{M : Type u_2}
[Zero M]
[ConditionallyCompleteLattice M]
{ι : Sort u_3}
[Nonempty ι]
[Finite ι]
{f : ι → α → M}
(hf : ∀ (i : ι), HasFiniteSupport (f i))
:
HasFiniteSupport fun (a : α) => ⨅ (i : ι), f i a
theorem
Function.HasFiniteMulSupport.pi
{α : Type u_1}
{M : Type u_2}
[One M]
{ι : Type u_3}
[Finite α]
{f : ι → α → M}
(hf : ∀ (a : α), HasFiniteMulSupport fun (x : ι) => f x a)
:
theorem
Function.HasFiniteSupport.pi
{α : Type u_1}
{M : Type u_2}
[Zero M]
{ι : Type u_3}
[Finite α]
{f : ι → α → M}
(hf : ∀ (a : α), HasFiniteSupport fun (x : ι) => f x a)
:
theorem
Function.HasFiniteMulSupport.sup'
{α : Type u_1}
{M : Type u_2}
[One M]
[SemilatticeSup M]
{ι : Type u_3}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, HasFiniteMulSupport (f i))
(hs : s.Nonempty)
:
HasFiniteMulSupport fun (a : α) => s.sup' hs fun (x : ι) => f x a
theorem
Function.HasFiniteSupport.sup'
{α : Type u_1}
{M : Type u_2}
[Zero M]
[SemilatticeSup M]
{ι : Type u_3}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, HasFiniteSupport (f i))
(hs : s.Nonempty)
:
HasFiniteSupport fun (a : α) => s.sup' hs fun (x : ι) => f x a
theorem
Function.HasFiniteMulSupport.inf'
{α : Type u_1}
{M : Type u_2}
[One M]
[SemilatticeInf M]
{ι : Type u_3}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, HasFiniteMulSupport (f i))
(hs : s.Nonempty)
:
HasFiniteMulSupport fun (a : α) => s.inf' hs fun (x : ι) => f x a
theorem
Function.HasFiniteSupport.inf'
{α : Type u_1}
{M : Type u_2}
[Zero M]
[SemilatticeInf M]
{ι : Type u_3}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, HasFiniteSupport (f i))
(hs : s.Nonempty)
:
HasFiniteSupport fun (a : α) => s.inf' hs fun (x : ι) => f x a
theorem
Function.HasFiniteMulSupport.comp_of_injective
{α : Type u_1}
{M : Type u_2}
[One M]
{β : Type u_3}
{f : β → M}
{g : α → β}
(hg : Injective g)
(hf : HasFiniteMulSupport f)
:
HasFiniteMulSupport (f ∘ g)
theorem
Function.HasFiniteSupport.comp_of_injective
{α : Type u_1}
{M : Type u_2}
[Zero M]
{β : Type u_3}
{f : β → M}
{g : α → β}
(hg : Injective g)
(hf : HasFiniteSupport f)
:
HasFiniteSupport (f ∘ g)
theorem
Function.HasFiniteMulSupport.fun_comp_of_injective
{α : Type u_1}
{M : Type u_2}
[One M]
{β : Type u_3}
{f : β → M}
{g : α → β}
(hg : Injective g)
(hf : HasFiniteMulSupport f)
:
HasFiniteMulSupport fun (a : α) => f (g a)
theorem
Function.HasFiniteSupport.fun_comp_of_injective
{α : Type u_1}
{M : Type u_2}
[Zero M]
{β : Type u_3}
{f : β → M}
{g : α → β}
(hg : Injective g)
(hf : HasFiniteSupport f)
:
HasFiniteSupport fun (a : α) => f (g a)
theorem
Function.HasFiniteMulSupport.of_comp
{α : Type u_1}
{M : Type u_2}
[One M]
{β : Type u_3}
{f : β → M}
{g : α → β}
[One β]
(hfg : HasFiniteMulSupport (f ∘ g))
(h : f 1 = 1)
(hf : Injective f)
:
theorem
Function.HasFiniteSupport.of_comp
{α : Type u_1}
{M : Type u_2}
[Zero M]
{β : Type u_3}
{f : β → M}
{g : α → β}
[Zero β]
(hfg : HasFiniteSupport (f ∘ g))
(h : f 0 = 0)
(hf : Injective f)
: