English
If α and β are finite and #α = #β, then #s^c = #t^c whenever #s = #t.
Русский
Если α и β конечны и #α = #β, то #s^c = #t^c при условии #s = #t.
LaTeX
$$∀ {α β} [Finite α] {s : Set α} {t : Set β} (h1 : #α = #β) (h : #s = #t), #(s^c : Set α) = #(t^c : Set β)$$
Lean4
theorem prod_eq_of_fintype {α : Type u} [h : Fintype α] (f : α → Cardinal.{v}) :
prod f = Cardinal.lift.{u} (∏ i, f i) := by
revert f
refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
· intro α β hβ e h f
letI := Fintype.ofEquiv β e.symm
rw [← e.prod_comp f, ← h]
exact mk_congr (e.piCongrLeft _).symm
· intro f
rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
· intro α hα h f
rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax.{v, u}, mk_out, ← Cardinal.prod, lift_prod,
Fintype.prod_option, lift_mul, ← h fun a => f (some a)]
simp only [lift_id]
