English
The type of dependent functions on the disjoint union s ∪ t is equivalent to the product of dependent functions on s and on t, reindexed by the union.
Русский
Тип зависимых функций над дизjoint-объединением s ∪ t эквивалентен произведению соответствующих типов над s и над t, скорректированному по объединению.
LaTeX
$$$\\\\big((\\\\forall i : s, \\\\alpha i) \\\\times \\\\forall i : t, \\\\alpha i) \\\\simeq \\\\forall i : (s \\\\u222a t), \\\\alpha i$$$
Lean4
/-- 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`. -/
def piFinsetUnion {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t) :
((∀ i : s, α i) × ∀ i : t, α i) ≃ ∀ i : (s ∪ t : Finset ι), α i :=
let e := Equiv.Finset.union s t h
sumPiEquivProdPi (fun b ↦ α (e b)) |>.symm.trans (.piCongrLeft (fun i : ↥(s ∪ t) ↦ α i) e)
