Documentation

Mathlib.Data.Nat.Order.Lemmas

Further lemmas about the natural numbers #

The distinction between this file and Mathlib.Algebra.Order.Ring.Nat is not particularly clear. They are separated for now to minimize the porting requirements for tactics during the transition to mathlib4. After Mathlib.Algebra.Order.Ring.Rat has been ported, please feel free to reorganize these two files.

Sets #

instance Nat.Subtype.orderBot (s : Set ) [DecidablePred fun (x : ) => x s] [h : Nonempty s] :
Equations
Equations
theorem Nat.Subtype.coe_bot {s : Set } [DecidablePred fun (x : ) => x s] [h : Nonempty s] :
= Nat.find
theorem Nat.set_eq_univ {S : Set } :
S = Set.univ 0 S kS, k + 1 S
theorem Nat.exists_not_and_succ_of_not_zero_of_exists {p : Prop} (H' : ¬p 0) (H : ∃ (n : ), p n) :
∃ (n : ), ¬p n p (n + 1)