Documentation

Mathlib.Data.Nat.Order.Lemmas

Further lemmas about the natural numbers #

The distinction between this file and Mathlib/Algebra/Order/Ring/Nat.lean 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)