move lemmas

src/analysis/normed/order/upper_lower.lean

@@ -22,52 +22,6 @@ We also prove lemmas specific to `ℝⁿ`. Those are helpful to prove that order
 are measurable.
 -/
 
-section
-variables {α : Type*} [linear_ordered_semifield α] {a : α}
-
-@[simp] lemma half_lt_self_iff : a / 2 < a ↔ 0 < a :=
-by rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
-
-end
-
-section
-variables {ι E : Type*} [fintype ι] [seminormed_group E] [nonempty ι]
-
-open function
-
-@[simp, to_additive pi_norm_const''] lemma pi_norm_const''' (a : E) : ‖const ι a‖ = ‖a‖ :=
-pi_norm_const' a
-
-@[simp, to_additive pi_nnnorm_const''] lemma pi_nnnorm_const''' (a : E) : ‖const ι a‖₊ = ‖a‖₊ :=
-pi_nnnorm_const' a
-
-end
-
-section
-variables {ι : Type*} [fintype ι] [nonempty ι] {ε : ℝ}
-
-open function metric
-
-lemma pi.exists_gt_mem_ball (x : ι → ℝ) (hε : 0 < ε) : ∃ y, x < y ∧ dist y x < ε :=
-begin
-  refine ⟨x + const ι (ε / 2), lt_add_of_pos_right _ $ by positivity, _⟩,
-  simpa [@pi_norm_const'' ι ℝ _ _ _ (ε / 2), abs_of_nonneg hε.le],
-end
-
-lemma pi.exists_lt_mem_ball (x : ι → ℝ) (hε : 0 < ε) : ∃ y, y < x ∧ dist y x < ε :=
-begin
-  refine ⟨x - const ι (ε / 2), sub_lt_self _ $ by positivity, _⟩,
-  simpa [@pi_norm_const'' ι ℝ _ _ _ (ε / 2), abs_of_nonneg hε.le],
-end
-
-end
-
-namespace real
-
-@[simp] lemma to_nnreal_abs (x : ℝ) : |x|.to_nnreal = x.nnabs := nnreal.coe_injective $ by simp
-
-end real
-
 open function metric set
 open_locale pointwise
 
@@ -279,12 +233,14 @@ begin
   have hx' := interior_subset hx,
   rw [mem_interior_iff_mem_nhds, metric.mem_nhds_iff] at hx,
   obtain ⟨ε, hε, hx⟩ := hx,
-  obtain ⟨y, hy, hyx⟩ := pi.exists_gt_mem_ball x hε,
-  exact hs.not_lt hx' (hx hyx) hy,
+  refine hs.not_lt hx' (hx _) (lt_add_of_pos_right _ (by positivity : 0 < const ι (ε / 2))),
+  simpa [const, @pi_norm_const ι ℝ _ _ _ (ε / 2), abs_of_nonneg hε.lt.le],
 end
 
-/-
-Note: The closure and frontier of an antichain might not be antichains. Take for example the union
+/-!
+#### Note
+
+The closure and frontier of an antichain might not be antichains. Take for example the union
 of the open segments from `(0, 2)` to `(1, 1)` and from `(2, 1)` to `(3, 0)`. `(1, 1)` and `(2, 1)`
 are comparable and both in the closure/frontier.
 -/

src/data/real/nnreal.lean

@@ -822,6 +822,8 @@ lemma nnabs_coe (x : ℝ≥0) : nnabs x = x := by simp
 lemma coe_to_nnreal_le (x : ℝ) : (to_nnreal x : ℝ) ≤ |x| :=
 max_le (le_abs_self _) (abs_nonneg _)
 
+@[simp] lemma to_nnreal_abs (x : ℝ) : |x|.to_nnreal = x.nnabs := nnreal.coe_injective $ by simp
+
 lemma cast_nat_abs_eq_nnabs_cast (n : ℤ) :
   (n.nat_abs : ℝ≥0) = nnabs n :=
 by { ext, rw [nnreal.coe_nat_cast, int.cast_nat_abs, real.coe_nnabs] }

src/order/bounds/basic.lean

@@ -62,6 +62,8 @@ def is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
 
 lemma mem_upper_bounds : a ∈ upper_bounds s ↔ ∀ x ∈ s, x ≤ a := iff.rfl
 lemma mem_lower_bounds : a ∈ lower_bounds s ↔ ∀ x ∈ s, a ≤ x := iff.rfl
+lemma mem_upper_bounds_iff_subset_Iic : a ∈ upper_bounds s ↔ s ⊆ Iic a := iff.rfl
+lemma mem_lower_bounds_iff_subset_Ici : a ∈ lower_bounds s ↔ s ⊆ Ici a := iff.rfl
 
 lemma bdd_above_def : bdd_above s ↔ ∃ x, ∀ y ∈ s, y ≤ x := iff.rfl
 lemma bdd_below_def : bdd_below s ↔ ∃ x, ∀ y ∈ s, x ≤ y := iff.rfl

src/topology/algebra/order/upper_lower.lean

@@ -23,16 +23,6 @@ The same lemmas are true in the additive/multiplicative worlds. To avoid code du
 provide `has_upper_lower_closure`, an ad hoc axiomatisation of the properties we need.
 -/
 
-section
-variables {α : Type*} [preorder α] {s : set α} {a : α}
-
-open set
-
-lemma mem_upper_bounds_iff_subset_Iic : a ∈ upper_bounds s ↔ s ⊆ Iic a := iff.rfl
-lemma mem_lower_bounds_iff_subset_Ici : a ∈ lower_bounds s ↔ s ⊆ Ici a := iff.rfl
-
-end
-
 open function set
 open_locale pointwise