Mathlib.Data.Nat.Cast.WithTop

Module docstring

{"# Lemma about the coercion ℕ → WithBot ℕ.

An orphaned lemma about casting from ℕ to WithBot ℕ, exiled here during the port to minimize imports of Algebra.Order.Ring.Rat. "}

instWellFoundedRelationWithTopNat instance

: WellFoundedRelation (WithTop ℕ)

Full source

instance : WellFoundedRelation (WithTop ℕ) where
  rel := (· < ·)
  wf := IsWellFounded.wf

Well-founded Relation on Extended Natural Numbers with Top

Informal description

The type `WithTop ℕ` (natural numbers extended with a top element) has a well-founded relation.

Nat.cast_withTop theorem

(n : ℕ) : Nat.cast n = WithTop.some n

Full source

theorem Nat.cast_withTop (n : ℕ) : Nat.cast n = WithTop.some n :=
  rfl

Canonical Embedding of Natural Numbers into Extended Natural Numbers with Top

Informal description

For any natural number $n$, the canonical embedding of $n$ into the type `WithTop ℕ` (natural numbers extended with a top element) is equal to the element `WithTop.some n`.

Nat.cast_withBot theorem

(n : ℕ) : Nat.cast n = WithBot.some n

Full source

theorem Nat.cast_withBot (n : ℕ) : Nat.cast n = WithBot.some n :=
  rfl

Canonical Embedding of Natural Numbers into Extended Natural Numbers with Bottom

Informal description

For any natural number $n$, the canonical embedding of $n$ into the type `WithBot ℕ` (natural numbers extended with a bottom element) is equal to the element `WithBot.some n$.