Theorems · Theorem · logic and foundations

Nat.Subtype.ofNat.eq_def

∀ (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst_1 : Infinite ↑s] (x : ℕ),
  Nat.Subtype.ofNat s x =
    match x with
    | 0 => ⊥
    | n.succ => Nat.Subtype.succ (Nat.Subtype.ofNat s n)

Defined in

Mathlib.Logic.Denumerable

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidablePredInfinite