Theorems · Theorem · logic and foundations

Denumerable.prod_ofNat_val

∀ {α : Type u_1} {β : Type u_2} [inst : Denumerable α] [inst_1 : Denumerable β] (n : ℕ),
  Denumerable.ofNat (α × β) n = (Denumerable.ofNat α (Nat.unpair n).1, Denumerable.ofNat β (Nat.unpair n).2)

Defined in

Mathlib.Logic.Denumerable

Cited by

1 results in Mathlib

Foundations

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

Assumes

DenumerableDenumerable