Stream: Is there code for X?
Ryan Lahfa (Feb 01 2021 at 14:45):
I'm looking for something like this:
import data.real.basic import data.nat.choose.basic lemma nat.const_le_find_of_not (p: ℕ → Prop) [decidable_pred p] (c: ℕ) (H: ∃ n, p n): (∀ (n: ℕ), n ≤ c → ¬ p n) → c ≤ nat.find H := sorry theorem mwe (exists_nat_unbdd: ∃ z : ℕ, abs (z: ℝ) > 1): 2 ≤ nat.find exists_nat_unbdd := sorry
It appears to me it does not exist in mathlib, should this exist? In this case, I believe I could finish the main theorem by some decidability tactic, am I wrong?
Floris van Doorn (Feb 01 2021 at 18:16):
The first inequality is an easy consequence of docs#nat.find_spec (by contradiction).
You can even make one of the
<. Is it worth adding? Not sure.
Floris van Doorn (Feb 01 2021 at 18:45):
I think the first lemma (and variants) is useful when formulated as
@[simp] lemma find_lt_iff (h : ∃ n : ℕ, p n) (n : ℕ) : nat.find h < n ↔ ∃ m < n, p m := ⟨λ h2, ⟨nat.find h, h2, nat.find_spec h⟩, λ ⟨m, hmn, hm⟩, (nat.find_min' h hm).trans_lt hmn⟩ @[simp] lemma find_le_iff (h : ∃ n : ℕ, p n) (n : ℕ) : nat.find h ≤ n ↔ ∃ m ≤ n, p m := by simp only [exists_prop, ← lt_succ_iff, find_lt_iff] @[simp] lemma le_find_iff (h : ∃ (n : ℕ), p n) (n : ℕ) : n ≤ nat.find h ↔ ∀ m < n, ¬ p m := by simp_rw [← not_lt, not_iff_comm, not_forall, not_not, find_lt_iff] @[simp] lemma lt_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n < nat.find h ↔ ∀ m ≤ n, ¬ p m := by simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]
Ryan Lahfa (Feb 03 2021 at 00:03):
Really, thanks a lot!
Ryan Lahfa (Feb 03 2021 at 00:04):
Indeed, I had the feeling they were not that far from find_spec or find_min, but it's really cool they are in mathlib now :)
Last updated: May 17 2021 at 15:13 UTC