Theorems · Theorem · logic and foundations

Cardinal.mk_pi_congr

∀ {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)

Defined in

Mathlib.SetTheory.Cardinal.Defs

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound