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] : OrderBot ↑s

Equations

• Nat.Subtype.orderBot s = OrderBot.mk ⋯

instance Nat.Subtype.semilatticeSup (s : Set ℕ) : SemilatticeSup ↑s

Equations

• Nat.Subtype.semilatticeSup s = let __src := Subtype.instLinearOrder s; let __src_1 := LinearOrder.toLattice; SemilatticeSup.mk ⋯ ⋯ ⋯

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 ∧ ∀ k ∈ S, 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)