Theorems · Definition · combinatorics
Equiv.piFinsetUnion
{ι : Type u_5} →
[inst : DecidableEq ι] →
(α : ι → Type u_4) →
{s t : Finset ι} → Disjoint s t → ((i : ↥s) → α ↑i) × ((i : ↥t) → α ↑i) ≃ ((i : ↥(s ∪ t)) → α ↑i)The type of dependent functions on the disjoint union of finsets s ∪ t is equivalent to the
type of pairs of functions on s and on t. This is similar to Equiv.sumPiEquivProdPi.
- Defined in
- Mathlib.Data.Finset.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Equivstatement and proof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Disjointstatement and proof · cited by 2,201
- Equiv.transproof · cited by 337
- Equiv.piCongrLeftproof · cited by 36
- Equiv.sumPiEquivProdPiproof · cited by 11
- Equiv.Finset.unionproof · cited by 9
Cited by5
Results whose statement or proof uses this declaration.
- Function.updateFinset_updateFinsetstatement and proof · cited by 2
- Function.update_updateFinsetstatement and proof · cited by 0
- Equiv.piFinsetUnion.congr_simpstatement and proof · cited by 0
- Equiv.piFinsetUnion_leftstatement · cited by 0
- Equiv.piFinsetUnion_rightstatement · cited by 0