feat(data/real/basic): make real irreducible

leanprover-community · Nov 1, 2018 · c08a3e5 · c08a3e5
1 parent ed84298
commit c08a3e5
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/analysis/complex.lean b/analysis/complex.lean
@@ -93,8 +93,8 @@ tendsto_of_uniform_continuous_subtype
     (λ x, id))
   (mem_nhds_sets
     (is_open_prod
-      (continuous_abs _ $ is_open_gt' _)
-      (continuous_abs _ $ is_open_gt' _))
+      (continuous_abs _ $ is_open_gt' (abs a₁ + 1))
+      (continuous_abs _ $ is_open_gt' (abs a₂ + 1)))
     ⟨lt_add_one (abs a₁), lt_add_one (abs a₂)⟩)
 
 lemma uniform_continuous_re : uniform_continuous re :=

diff --git a/analysis/real.lean b/analysis/real.lean
@@ -182,8 +182,8 @@ tendsto_of_uniform_continuous_subtype
     (λ x, id))
   (mem_nhds_sets
     (is_open_prod
-      (real.continuous_abs _ $ is_open_gt' _)
-      (real.continuous_abs _ $ is_open_gt' _))
+      (real.continuous_abs _ $ is_open_gt' (abs a₁ + 1))
+      (real.continuous_abs _ $ is_open_gt' (abs a₂ + 1)))
     ⟨lt_add_one (abs a₁), lt_add_one (abs a₂)⟩)
 
 instance : topological_ring ℝ :=

diff --git a/data/real/basic.lean b/data/real/basic.lean
@@ -254,6 +254,8 @@ theorem exists_sup (S : set ℝ) : (∃ x, x ∈ S) → (∃ x, ∀ y ∈ S, y
     (lt_of_le_of_lt hy $ sub_lt_iff_lt_add.1 $ hf₂ _ k0 _ yS)
 end
 
+attribute [irreducible] real
+
 noncomputable def Sup (S : set ℝ) : ℝ :=
 if h : (∃ x, x ∈ S) ∧ (∃ x, ∀ y ∈ S, y ≤ x)
 then classical.some (exists_sup S h.1 h.2) else 0