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 were separated for now to minimize the porting requirements for tactics during the transition to mathlib4. Please feel free to reorganize these two files.

Sets #

instance Nat.Subtype.orderBot (s : Set ) [DecidablePred fun (x : ) => x s] [h : Nonempty s] :
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)