Merge pull request #10 from adomasbaliuka/adomas_approx_lemmas_for_co…

…nversions Adds lemmas mem_approx_natCast and mem_approx_natCast
girving · Aug 26, 2024 · 0db0309 · 0db0309
2 parents 76923ad + 0ebb837
commit 0db0309
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Interval/Interval/Conversion.lean b/Interval/Interval/Conversion.lean
@@ -102,6 +102,10 @@ instance {n : ℕ} [n.AtLeastTwo] : OfNat Interval n := ⟨.ofNat n⟩
   simp only [OfScientific.ofScientific]
   apply approx_ofRat
 
+@[approx] lemma mem_approx_natCast (n : ℕ) : (n : ℝ) ∈ approx (n : Interval) := approx_ofNat _
+
+@[approx] lemma mem_approx_intCast (n : ℤ) : (n : ℝ) ∈ approx (n : Interval) := approx_ofInt _
+
 /-- `n.lo ≤ n` -/
 lemma ofNat_le (n : ℕ) : (ofNat n).lo.val ≤ n := by
   by_cases m : ofNat n = nan