Theorems · Theorem · logic and foundations

Denumerable.sigma_ofNat_val

∀ {α : Type u_1} [inst : Denumerable α] {γ : α → Type u_3} [inst_1 : (a : α) → Denumerable (γ a)] (n : ℕ),
  Denumerable.ofNat (Sigma γ) n =
    ⟨Denumerable.ofNat α (Nat.unpair n).1,
      Denumerable.ofNat (γ (Denumerable.ofNat α (Nat.unpair n).1)) (Nat.unpair n).2⟩

Defined in

Mathlib.Logic.Denumerable

Cited by

7 results in Mathlib

Foundations

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

Assumes

DenumerableDenumerable