Abstract file for real.lean

real.alean

def zero_nhd : filter ℚ :=
lemma mem_zero_nhd {r : ℚ} (h : 0 < r) : {q | abs q < r} ∈ zero_nhd.sets :=
lemma mem_zero_nhd_le {r : ℚ} (h : 0 < r) : {q | abs q ≤ r} ∈ zero_nhd.sets :=
lemma mem_zero_nhd_iff {s : set ℚ} : s ∈ zero_nhd.sets ↔ ∃r>0, ∀q:ℚ, abs q < r → q ∈ s :=
lemma tendsto_zero_nhds {m : α → ℚ} {f : filter α} (hm : ∀r>0, {a | abs (m a) < r} ∈ f.sets) :
  tendsto m f zero_nhd :=
lemma pure_zero_le_zero_nhd : pure 0 ≤ zero_nhd :=
lemma tendsto_neg_rat_zero : tendsto has_neg.neg zero_nhd zero_nhd :=
lemma tendsto_add_rat_zero : tendsto (λp:ℚ×ℚ, p.1 + p.2) (filter.prod zero_nhd zero_nhd) zero_nhd :=
lemma tendsto_add_rat_zero' {f g : α → ℚ} {x : filter α}
  (hf : tendsto f x zero_nhd) (hg : tendsto g x zero_nhd) : tendsto (λa, f a + g a) x zero_nhd :=
lemma tendsto_sub_rat' {f g : α → ℚ} {x : filter α}
  (hf : tendsto f x zero_nhd) (hg : tendsto g x zero_nhd) : tendsto (λa, f a - g a) x zero_nhd :=
lemma tendsto_mul_bnd_rat {f : filter ℚ} {r : ℚ} (hr : 0 < r) (hf : {x : ℚ | abs x ≤ r} ∈ f.sets) :
  tendsto (λp:ℚ×ℚ, p.1 * p.2) (filter.prod zero_nhd f) zero_nhd :=
lemma tendsto_mul_bnd_rat' {r : ℚ} {f g : α → ℚ} {x : filter α}
  (hr : 0 < r) (hy : {x : α | abs (g x) ≤ r} ∈ x.sets) (hf : tendsto f x zero_nhd) :
  tendsto (λa, f a * g a) x zero_nhd :=
lemma tendsto_mul_rat' {f g : α → ℚ} {x : filter α}
  (hf : tendsto f x zero_nhd) (hg : tendsto g x zero_nhd) : tendsto (λa, f a * g a) x zero_nhd :=
lemma uniformity_rat : uniformity = zero_nhd.vmap (λp:ℚ×ℚ, p.1 - p.2) :=
lemma mem_uniformity_rat {r : ℚ} (h : 0 < r) :
  {x:(ℚ × ℚ) | abs (x.1 - x.2) < r} ∈ (@uniformity ℚ _).sets :=
lemma uniform_continuous_rat [uniform_space α] {f : α → ℚ}
  (hf : tendsto (λp:α×α, f p.1 - f p.2) uniformity zero_nhd ) : uniform_continuous f :=
lemma tendsto_sub_uniformity_zero_nhd : tendsto (λp:(ℚ×ℚ), p.1 - p.2) uniformity zero_nhd :=
lemma tendsto_sub_uniformity_zero_nhd' {p : α → ℚ} {q : α → ℚ} {f : filter α}
  (h : tendsto (λx, (p x, q x)) f uniformity) : tendsto (λa, p a - q a) f zero_nhd :=
lemma uniform_continuous_add_rat : uniform_continuous (λp : ℚ × ℚ, p.1 + p.2) :=
lemma uniform_continuous_neg_rat : uniform_continuous (λr:ℚ, -r) :=
lemma nhds_eq_map_zero_nhd {r : ℚ} : nhds r = map (λx, x + r) zero_nhd :=
lemma uniform_embedding_add_rat {r : ℚ} : uniform_embedding (λp:ℚ, p + r) :=
lemma uniform_embedding_mul_rat {q : ℚ} (hq : q ≠ 0) : uniform_embedding ((*) q) :=
lemma nhds_0_eq_zero_nhd : nhds 0 = zero_nhd :=
lemma uniform_continuous_inv_pos_rat {r : ℚ} (hr : 0 < r) :
  uniform_continuous (λp:{q:ℚ // r ≤ q}, p.1⁻¹) :=
lemma tendsto_of_uniform_continuous_subtype
  [uniform_space α] [uniform_space β] {f: α → β} {p : α → Prop} {a : α}
  (hf : uniform_continuous (λx:{a // p a}, f x.val)) (ha : {a | p a} ∈ (nhds a).sets) :
  tendsto f (nhds a) (nhds (f a)) :=
lemma uniform_continuous_rat' {f : ℚ → ℚ}
  (h : ∀i>0, ∃j>0, ∀a₁ a₂, abs (a₁ - a₂) < j → abs (f a₁ - f a₂) < i) : uniform_continuous f :=
lemma uniform_continuous_abs_rat : uniform_continuous (abs : ℚ → ℚ) :=
lemma continuous_abs_rat : continuous (abs : ℚ → ℚ) :=
lemma tendsto_inv_pos_rat {r : ℚ} (hr : 0 < r) : tendsto (λq, q⁻¹) (nhds r) (nhds r⁻¹) :=
lemma tendsto_inv_rat {r : ℚ} (hr : r ≠ 0) : tendsto (λq, q⁻¹) (nhds r) (nhds r⁻¹) :=
lemma uniform_continuous_mul_rat {r₁ r₂ : ℚ} (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) :
  uniform_continuous (λp:{q:ℚ // abs q ≤ r₁}×{q:ℚ // abs q ≤ r₂}, p.1.1 * p.2.1) :=
lemma uniform_continuous_swap [uniform_space α] [uniform_space β] {p : α → Prop} {q : β → Prop} :
  uniform_continuous (λx:{x:α×β // p x.1 ∧ q x.2},
     ((⟨x.val.1, x.property.left⟩ : {x // p x}), (⟨x.val.2, x.property.right⟩ : {x // q x}))) :=
lemma tendsto_mul_rat {r q : ℚ} : tendsto (λp:ℚ×ℚ, p.1 * p.2) (nhds (r, q)) (nhds (r * q)) :=
lemma totally_bounded_01_rat : totally_bounded {q:ℚ | 0 ≤ q ∧ q ≤ 1} :=
def real : Type :=
def of_rat (q : ℚ) : ℝ :=
lemma of_rat_injective : function.injective of_rat
| a b h :=
lemma of_rat_inj {a b : ℚ} : of_rat a = of_rat b ↔ a = b :=
lemma uniform_embedding_of_rat : uniform_embedding of_rat :=
lemma dense_embedding_of_rat : dense_embedding of_rat :=
lemma dense_embedding_of_rat_of_rat : dense_embedding (λp:ℚ×ℚ, (of_rat p.1, of_rat p.2)) :=
def lift_rat_fun (f : ℚ → ℚ) : ℝ → ℝ :=
def lift_rat_op (f : ℚ → ℚ → ℚ) (a : ℝ) (b : ℝ) : ℝ :=
lemma lift_rat_fun_of_rat {r : ℚ} {f : ℚ → ℚ} (hf : tendsto f (nhds r) (nhds (f r))) :
  lift_rat_fun f (of_rat r) = of_rat (f r) :=
lemma lift_rat_op_of_rat_of_rat {r₁ r₂: ℚ} {f : ℚ → ℚ → ℚ}
  (hf : tendsto (λp:ℚ×ℚ, f p.1 p.2) (nhds (r₁, r₂)) (nhds (f r₁ r₂))) :
  lift_rat_op f (of_rat r₁) (of_rat r₂) = of_rat (f r₁ r₂) :=
lemma of_rat_zero : 0 = of_rat 0 :=
lemma of_rat_one : 1 = of_rat 1 :=
lemma of_rat_neg {r : ℚ} : - of_rat r = of_rat (- r) :=
lemma of_rat_add {r₁ r₂ : ℚ} : of_rat r₁ + of_rat r₂ = of_rat (r₁ + r₂) :=
lemma of_rat_sub {r₁ r₂ : ℚ} : of_rat r₁ - of_rat r₂ = of_rat (r₁ - r₂) :=
lemma of_rat_mul {r₁ r₂ : ℚ} : of_rat r₁ * of_rat r₂ = of_rat (r₁ * r₂) :=
lemma of_rat_inv {r : ℚ} : (of_rat r)⁻¹ = of_rat r⁻¹ :=
lemma uniform_continuous_neg_real : uniform_continuous (λp:ℝ, - p) :=
lemma uniform_continuous_add_real : uniform_continuous (λp:ℝ×ℝ, p.1 + p.2) :=
lemma continuous_neg_real : continuous (λp:ℝ, - p) :=
lemma continuous_add_real' : continuous (λp:ℝ×ℝ, p.1 + p.2) :=
lemma continuous_add_real [topological_space α] {f g : α → ℝ}
  (hf : continuous f) (hg : continuous g) : continuous (λx, f x + g x) :=
def nonneg : set ℝ :=
lemma of_rat_mem_nonneg {q : ℚ} (h : 0 ≤ q) : of_rat q ∈ nonneg :=
lemma of_rat_mem_nonneg_iff {q : ℚ} : of_rat q ∈ nonneg ↔ 0 ≤ q :=
lemma of_rat_le_of_rat {q₁ q₂ : ℚ} : of_rat q₁ ≤ of_rat q₂ ↔ q₁ ≤ q₂ :=
lemma two_eq_of_rat_two : 2 = of_rat 2 :=
lemma mem_nonneg_of_continuous2 {f : ℝ → ℝ → ℝ} {a b : ℝ}
  (hf : continuous (λp:ℝ×ℝ, f p.1 p.2)) (ha : a ∈ nonneg) (hb : b ∈ nonneg)
  (h : ∀{a b : ℚ}, 0 ≤ a → 0 ≤ b → f (of_rat a) (of_rat b) ∈ nonneg) :
  (f a b) ∈ nonneg :=
lemma zero_le_iff_nonneg {r : ℝ} : 0 ≤ r ↔ r ∈ nonneg :=
def abs_real :=
lemma uniform_continuous_abs_real' : uniform_continuous abs_real :=
lemma continuous_abs_real' : continuous abs_real :=
lemma of_rat_abs_real {r} : abs_real (of_rat r) = of_rat (abs r) :=
lemma abs_real_neg : ∀{r}, abs_real (- r) = abs_real r :=
lemma abs_real_of_nonneg {r:ℝ} : 0 ≤ r → abs_real r = r :=
lemma nonneg_antisymm {r : ℝ} (hp : r ∈ nonneg) (hn : -r ∈ nonneg) : r = 0 :=
lemma preimage_neg_real : preimage (has_neg.neg : ℝ → ℝ) = image (has_neg.neg : ℝ → ℝ) :=
lemma neg_preimage_closure {s : set ℝ} : (λr:ℝ, -r) ⁻¹' closure s = closure ((λr:ℝ, -r) '' s) :=
lemma of_rat_lt {q₁ q₂ : ℚ} : of_rat q₁ < of_rat q₂ ↔ q₁ < q₂ :=
lemma add_le_add_left_iff {a b c : ℝ} : (c + a ≤ c + b) ↔ a ≤ b :=
lemma preimage_neg_rat : preimage (has_neg.neg : ℚ → ℚ) = image (has_neg.neg : ℚ → ℚ) :=
lemma map_neg_real : map (has_neg.neg : ℝ → ℝ) = vmap (has_neg.neg : ℝ → ℝ) :=
lemma map_neg_rat : map (has_neg.neg : ℚ → ℚ) = vmap (has_neg.neg : ℚ → ℚ) :=
lemma is_closed_le_real [topological_space α] {f g : α → ℝ}
  (hf : continuous f) (hg : continuous g) : is_closed {a:α | f a ≤ g a} :=
lemma is_open_lt_real [topological_space α] {f g : α → ℝ}
  (hf : continuous f) (hg : continuous g) : is_open {a | f a < g a} :=
lemma abs_real_eq_abs : abs_real = abs :=
lemma uniform_continuous_abs_real : uniform_continuous (abs : ℝ → ℝ) :=
lemma continuous_abs_real : continuous (abs : ℝ → ℝ) :=
lemma of_rat_abs {q : ℚ} : of_rat (abs q) = abs (of_rat q) :=
lemma min_of_rat_of_rat {a b : ℚ} : min (of_rat a) (of_rat b) = of_rat (min a b) :=
lemma max_of_rat_of_rat {a b : ℚ} : max (of_rat a) (of_rat b) = of_rat (max a b) :=
lemma exists_pos_of_rat {r : ℝ} (hr : 0 < r) : ∃q:ℚ, 0 < q ∧ of_rat q < r :=
lemma mem_uniformity_real_iff {s : set (ℝ × ℝ)} :
  s ∈ (@uniformity ℝ _).sets ↔ (∃e>0, ∀r₁ r₂:ℝ, abs (r₁ - r₂) < of_rat e → (r₁, r₂) ∈ s) :=
lemma nhds_eq_real {x : ℝ} : nhds x = (⨅r > 0, principal {p | abs (x - p) < r}) :=
lemma exists_lt_of_rat (r : ℝ) : ∃q:ℚ, r < of_rat q :=
lemma exists_gt_of_rat (r : ℝ) : ∃q:ℚ, of_rat q < r :=
lemma closure_of_rat_image_le_eq {q : ℚ} : closure (of_rat '' {x | q ≤ x}) = {r | of_rat q ≤ r } :=
lemma closure_of_rat_image_le_le_eq {a b : ℚ} (hab : a ≤ b) :
  closure (of_rat '' {q:ℚ | a ≤ q ∧ q ≤ b}) = {r:ℝ | of_rat a ≤ r ∧ r ≤ of_rat b} :=
lemma continuous_mul_real : continuous (λp:ℝ×ℝ, p.1 * p.2) :=
lemma continuous_mul_real' [topological_space α] {f g : α → ℝ} (hf : continuous f) (hg : continuous g) :
  continuous (λx, f x * g x) :=
lemma tendsto_inv_real {r : ℝ} (hr : r ≠ 0) : tendsto has_inv.inv (nhds r) (nhds r⁻¹) :=
lemma continuous_inv_real' : continuous (λa:{r:ℝ // r ≠ 0}, a.val⁻¹) :=
lemma continuous_inv_real [topological_space α] {f : α → ℝ} (h : ∀a, f a ≠ 0) (hf : continuous f) :
  continuous (λa, (f a)⁻¹) :=
lemma closure_compl_zero_image_univ :
  closure ((λp:{q:ℚ // q ≠ 0},
    (⟨of_rat p.val, assume h, p.2 $ dense_embedding_of_rat.inj _ _ h⟩ : {r:ℝ // r ≠ 0})) '' univ) = univ :=
lemma mul_nonneg {a b : ℝ} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
theorem coe_rat_eq_of_rat (r : ℚ) : ↑r = of_rat r :=
lemma exists_rat_btwn {r p : ℝ} (h : r < p) : ∃q : ℚ, r < (q:ℝ) ∧ (q:ℝ) < p :=
lemma exists_lt_rat (r : ℝ) : ∃q:ℚ, r < q :=
lemma exists_rat_lt (r : ℝ) : ∃q:ℚ, (q : ℝ) < r :=
lemma exists_lt_nat (r : ℝ) : ∃n : ℕ, r < n :=
lemma compact_ivl {a b : ℝ} : compact {r:ℝ | a ≤ r ∧ r ≤ b } :=
lemma exists_supremum_real {s : set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ upper_bounds s) :
  ∃x, is_lub s x :=