Theorems · Theorem
Function.HasFiniteSupport.pi
∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {ι : Type u_3} [Finite α] {f : ι → α → M},
(∀ (a : α), Function.HasFiniteSupport fun x => f x a) → Function.HasFiniteSupport f- Defined in
- Mathlib.Algebra.FiniteSupport.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finitestatement and proof · cited by 3,029
- Function.supportproof · cited by 610
- Set.Finite.subsetproof · cited by 285
- Set.mem_iUnionproof · cited by 212
- Function.HasFiniteSupportstatement and proof · cited by 113
- Function.mem_supportproof · cited by 54
- Function.ne_iffproof · cited by 40
- Set.finite_iUnionproof · cited by 14
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.