feat(topology/topological_structures,ennreal): show continuity of of_ennreal and of_real

Author: johoelzl

data/set/basic.lean

@@ -543,14 +543,18 @@ by finish [set_eq_def, iff_def, mem_image_eq]
 theorem image_empty (f : α → β) : f '' ∅ = ∅ :=
 by finish [set_eq_def, mem_image_eq]
 
-lemma image_inter {f : α → β} {s t : set α} (h : ∀ x y, f x = f y → x = y) :
+lemma image_inter_on {f : α → β} {s t : set α} (h : ∀x∈t, ∀y∈s, f x = f y → x = y) :
   f '' s ∩ f '' t = f '' (s ∩ t) :=
 subset.antisymm
   (assume b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩,
-    have a₂ = a₁, from h a₂ a₁ $ h₁.symm ▸ h₂.symm ▸ rfl,
+    have a₂ = a₁, from h _ ha₂ _ ha₁ (by simp *),
     ⟨a₁, ⟨ha₁, this ▸ ha₂⟩, h₁⟩)
   (subset_inter (mono_image $ inter_subset_left _ _) (mono_image $ inter_subset_right _ _))
 
+lemma image_inter {f : α → β} {s t : set α} (h : ∀ x y, f x = f y → x = y) :
+  f '' s ∩ f '' t = f '' (s ∩ t) :=
+image_inter_on (assume x _ y _, h x y)
+
 @[simp] lemma image_singleton {f : α → β} {a : α} : f '' {a} = {f a} :=
 set.ext $ λ x, by simp [image]; rw eq_comm
 
@@ -664,7 +668,7 @@ This function is more flexiable as `f '' univ`, as the image requires that the d
 and not an arbitrary Sort. -/
 def range (f : ι → α) : set α := {x | ∃y, f y = x}
 
-lemma mem_range {i : ι} : f i ∈ range f := ⟨i, rfl⟩ 
+lemma mem_range {i : ι} : f i ∈ range f := ⟨i, rfl⟩
 
 lemma forall_range_iff {p : α → Prop} : (∀a∈range f, p a) ↔ (∀i, p (f i)) :=
 ⟨assume h i, h (f i) mem_range, assume h a ⟨i, (hi : f i = a)⟩, hi ▸ h i⟩

order/filter.lean

@@ -454,7 +454,7 @@ f.upwards_sets hs $ assume x hx, ⟨x, hx, rfl⟩
 
 @[simp] lemma map_id : filter.map id f = f :=
 filter_eq $ rfl
-  
+
 @[simp] lemma map_compose : filter.map m' ∘ filter.map m = filter.map (m' ∘ m) :=
 funext $ assume _, filter_eq $ rfl
 
@@ -537,6 +537,23 @@ le_antisymm
   (assume s ⟨t, (h₁ : preimage m t ∈ f.sets), (h₂ : preimage m t ⊆ s)⟩,
     f.upwards_sets h₁ h₂)
 
+lemma le_of_map_le_map_inj' {f g : filter α} {m : α → β} {s : set α}
+  (hsf : s ∈ f.sets) (hsg : s ∈ g.sets) (hm : ∀x∈s, ∀y∈s, m x = m y → x = y)
+  (h : map m f ≤ map m g) : f ≤ g :=
+assume t ht,
+  have m ⁻¹' (m '' (s ∩ t)) ∈ f.sets, from h $ image_mem_map (inter_mem_sets hsg ht),
+  f.upwards_sets (inter_mem_sets hsf this) $
+    assume a ⟨has, b, ⟨hbs, hb⟩, h⟩,
+    have b = a, from hm _ hbs _ has h,
+    this ▸ hb
+
+lemma eq_of_map_eq_map_inj' {f g : filter α} {m : α → β} {s : set α}
+  (hsf : s ∈ f.sets) (hsg : s ∈ g.sets) (hm : ∀x∈s, ∀y∈s, m x = m y → x = y)
+  (h : map m f = map m g) : f = g :=
+le_antisymm
+  (le_of_map_le_map_inj' hsf hsg hm $ le_of_eq h)
+  (le_of_map_le_map_inj' hsg hsf hm $ le_of_eq h.symm)
+
 lemma map_inj {f g : filter α} {m : α → β} (hm : ∀ x y, m x = m y → x = y) (h : map m f = map m g) :
   f = g :=
 have vmap m (map m f) = vmap m (map m g), by rw h,
@@ -596,30 +613,43 @@ le_antisymm
       from infi_le_of_le i $ by simp; assumption,
     by simp at this; assumption)
 
-lemma map_binfi_eq {ι : Type w} {f : ι → filter α} {m : α → β} {s : set ι}
-  (h : directed_on (λx y, f x ≤ f y) s) (ne : ∃i, i ∈ s) : map m (⨅i∈s, f i) = (⨅i∈s, map m (f i)) :=
+lemma map_binfi_eq {ι : Type w} {f : ι → filter α} {m : α → β} {p : ι → Prop}
+  (h : directed_on (λx y, f x ≤ f y) {x | p x}) (ne : ∃i, p i) :
+  map m (⨅i (h : p i), f i) = (⨅i (h: p i), map m (f i)) :=
 let ⟨i, hi⟩ := ne in
-calc map m (⨅i∈s, f i) = map m (⨅i:{i // i ∈ s}, f i.val) : by simp [infi_subtype]
-  ... = (⨅i:{i // i ∈ s}, map m (f i.val)) : map_infi_eq
+calc map m (⨅i (h : p i), f i) = map m (⨅i:subtype p, f i.val) : by simp [infi_subtype]
+  ... = (⨅i:subtype p, map m (f i.val)) : map_infi_eq
     (assume ⟨x, hx⟩ ⟨y, hy⟩, match h x hx y hy with ⟨z, h₁, h₂, h₃⟩ := ⟨⟨z, h₁⟩, h₂, h₃⟩ end)
     ⟨⟨i, hi⟩⟩
-  ... = (⨅i∈s, map m (f i)) : by simp [infi_subtype]
+  ... = (⨅i (h : p i), map m (f i)) : by simp [infi_subtype]
 
-lemma map_inf {f g : filter α} {m : α → β} (h : ∀ x y, m x = m y → x = y) :
-  map m (f ⊓ g) = map m f ⊓ map m g :=
+lemma map_inf' {f g : filter α} {m : α → β} {t : set α} (htf : t ∈ f.sets) (htg : t ∈ g.sets)
+  (h : ∀x∈t, ∀y∈t, m x = m y → x = y) : map m (f ⊓ g) = map m f ⊓ map m g :=
 le_antisymm
   (le_inf (map_mono inf_le_left) (map_mono inf_le_right))
   (assume s hs,
   begin
     simp [map, mem_inf_sets] at hs,
     simp [map, mem_inf_sets],
     exact (let ⟨t₁, h₁, t₂, h₂, hs⟩ := hs in
-      ⟨m '' t₁, f.upwards_sets h₁ $ image_subset_iff_subset_preimage.mp $ subset.refl _,
-        m '' t₂,
-        by rwa [set.image_inter h, image_subset_iff_subset_preimage],
-        g.upwards_sets h₂ $ image_subset_iff_subset_preimage.mp $ subset.refl _⟩)
+      have m '' (t₁ ∩ t) ∩ m '' (t₂ ∩ t) ⊆ s,
+      begin
+        rw [image_inter_on],
+        apply image_subset_iff_subset_preimage.mpr _,
+        exact assume x ⟨⟨h₁, _⟩, h₂, _⟩, hs ⟨h₁, h₂⟩,
+        exact assume x ⟨_, hx⟩ y ⟨_, hy⟩, h x hx y hy
+      end,
+      ⟨m '' (t₁ ∩ t),
+        f.upwards_sets (inter_mem_sets h₁ htf) $ image_subset_iff_subset_preimage.mp $ subset.refl _,
+        m '' (t₂ ∩ t),
+        this,
+        g.upwards_sets (inter_mem_sets h₂ htg) $ image_subset_iff_subset_preimage.mp $ subset.refl _⟩)
   end)
 
+lemma map_inf {f g : filter α} {m : α → β} (h : ∀ x y, m x = m y → x = y) :
+  map m (f ⊓ g) = map m f ⊓ map m g :=
+map_inf' univ_mem_sets univ_mem_sets (assume x _ y _, h x y)
+
 /- bind equations -/
 
 lemma mem_bind_sets {β : Type u} {s : set β} {f : filter α} {m : α → filter β} :
@@ -734,6 +764,10 @@ lemma tendsto_infi' {f : α → β} {x : ι → filter α} {y : filter β} (i :
   (h : tendsto f (x i) y) : tendsto f (⨅i, x i) y :=
 le_trans (map_mono $ infi_le _ _) h
 
+lemma tendsto_principal {f : α → β} {a : filter α} {s : set β}
+  (h : {a | f a ∈ s} ∈ a.sets) : tendsto f a (principal s) :=
+by simp [tendsto]; exact h
+
 lemma tendsto_principal_principal {f : α → β} {s : set α} {t : set β}
   (h : ∀a∈s, f a ∈ t) : tendsto f (principal s) (principal t) :=
 by simp [tendsto, image_subset_iff_subset_preimage]; exact h

order/lattice.lean

@@ -60,6 +60,9 @@ theorem eq_top_iff : a = ⊤ ↔ ⊤ ≤ a :=
 @[simp] theorem top_le_iff : ⊤ ≤ a ↔ a = ⊤ :=
 ⟨top_unique, λ h, h.symm ▸ le_refl ⊤⟩
 
+@[simp] theorem not_top_lt : ¬ ⊤ < a :=
+assume h, lt_irrefl a (lt_of_le_of_lt le_top h)
+
 end order_top
 
 class order_bot (α : Type u) extends has_bot α, partial_order α :=
@@ -80,6 +83,9 @@ theorem eq_bot_iff : a = ⊥ ↔ a ≤ ⊥ :=
 @[simp] theorem le_bot_iff : a ≤ ⊥ ↔ a = ⊥ :=
 ⟨bot_unique, assume h, h.symm ▸ le_refl ⊥⟩
 
+@[simp] theorem not_lt_bot : ¬ a < ⊥ :=
+assume h, lt_irrefl a (lt_of_lt_of_le h bot_le)
+
 theorem neq_bot_of_le_neq_bot {a b : α} (hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥ :=
 assume ha, hb $ bot_unique $ ha ▸ hab
 

topology/ennreal.lean

@@ -15,6 +15,14 @@ universe u
 lemma zero_le_mul {α : Type u} [ordered_semiring α] {a b : α} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
 mul_nonneg
 
+instance linear_ordered_semiring.to_top_order {α : Type*} [linear_ordered_semiring α] :
+  no_top_order α :=
+⟨assume a, ⟨a + 1, lt_add_of_pos_right _ zero_lt_one⟩⟩
+
+instance linear_ordered_semiring.to_bot_order {α : Type*} [linear_ordered_ring α] :
+  no_bot_order α :=
+⟨assume a, ⟨a - 1, sub_lt_iff.mpr $ lt_add_of_pos_right _ zero_lt_one⟩⟩
+
 lemma inv_pos {α : Type*} [linear_ordered_field α] {r : α} : 0 < r → 0 < r⁻¹ :=
 by rw [inv_eq_one_div]; exact div_pos_of_pos_of_pos zero_lt_one
 
@@ -523,35 +531,80 @@ instance : t2_space ennreal := by apply_instance
 lemma continuous_of_real : continuous of_real :=
 have ∀x:ennreal, is_open {a : ℝ | x < of_real a},
   from forall_ennreal.mpr ⟨assume r hr,
-    begin
-      simp [of_real_lt_of_real_iff_cases],
-      exact is_open_and
-        (is_open_lt continuous_const continuous_id)
-        (is_open_lt continuous_const continuous_id)
-    end,
+    by simp [of_real_lt_of_real_iff_cases]; exact is_open_and (is_open_lt' r) (is_open_lt' 0),
     by simp⟩,
 have ∀x:ennreal, is_open {a : ℝ | of_real a < x},
   from forall_ennreal.mpr ⟨assume r hr,
-    begin
-      simp [of_real_lt_of_real_iff_cases],
-      exact is_open_and (is_open_lt continuous_id continuous_const) is_open_const
-    end,
+    by simp [of_real_lt_of_real_iff_cases]; exact is_open_and (is_open_gt' r) is_open_const,
     by simp [is_open_const]⟩,
 continuous_generated_from $ begin simp [or_imp_distrib, *] {contextual := tt} end
 
-/- TODO:
+lemma tendsto_of_real : tendsto of_real (nhds r) (nhds (of_real r)) :=
+continuous_iff_tendsto.mp continuous_of_real r
+
+lemma tendsto_of_ennreal (hr : 0 ≤ r) : tendsto of_ennreal (nhds (of_real r)) (nhds r) :=
+tendsto_orderable_unbounded (no_top _) (no_bot _) $
+assume l u hl hu,
+by_cases
+  (assume hr : r = 0,
+    have hl : l < 0, by rw [hr] at hl; exact hl,
+    have hu : 0 < u, by rw [hr] at hu; exact hu,
+    have nhds (of_real r) = (⨅l (h₂ : 0 < l), principal {x | x < l}),
+      from calc nhds (of_real r) = nhds ⊥ : by simp [hr]; refl
+        ... = (⨅u (h₂ : 0 < u), principal {x | x < u}) : nhds_bot_orderable,
+    have {x | x < of_real u} ∈ (nhds (of_real r)).sets,
+      by rw [this];
+      from mem_infi_sets (of_real u) (mem_infi_sets (by simp *) (subset.refl _)),
+    ((nhds (of_real r)).upwards_sets this $ forall_ennreal.mpr $
+        by simp [le_of_lt, hu, hl] {contextual := tt}; exact assume p hp _, lt_of_lt_of_le hl hp))
+  (assume hr_ne : r ≠ 0,
+    have hu0 : 0 < u, from lt_of_le_of_lt hr hu,
+    have hu_nn: 0 ≤ u, from le_of_lt hu0,
+    have hr' : 0 < r, from lt_of_le_of_ne hr hr_ne.symm,
+    have hl' : ∃l, l < of_real r, from ⟨0, by simp [hr, hr']⟩,
+    have hu' : ∃u, of_real r < u, from ⟨of_real u, by simp [hr, hu_nn, hu]⟩,
+    begin
+      rw [mem_nhds_lattice_unbounded hu' hl'],
+      existsi (of_real l), existsi (of_real u),
+      simp [*, of_real_lt_of_real_iff_cases, forall_ennreal] {contextual := tt}
+    end)
+
 lemma nhds_of_real_eq_map_of_real_nhds {r : ℝ} (hr : 0 ≤ r) :
-  nhds (of_real r) = (nhds r ⊓ principal {x | 0 ≤ x}).map of_real :=
+  nhds (of_real r) = (nhds r).map of_real :=
+have h₁ : {x | x < ∞} ∈ (nhds (of_real r)).sets,
+  from mem_nhds_sets (is_open_gt' ∞) of_real_lt_infty,
+have h₂ : {x | x < ∞} ∈ ((nhds r).map of_real).sets,
+  from mem_map.mpr $ univ_mem_sets' $ assume a, of_real_lt_infty,
+have h : ∀x<∞, ∀y<∞, of_ennreal x = of_ennreal y → x = y,
+  by simp [forall_ennreal] {contextual:=tt},
 le_antisymm
-  _
-  _
-
+  (by_cases
+    (assume (hr : r = 0) s (hs : {x | of_real x ∈ s} ∈ (nhds r).sets),
+      have hs : {x | of_real x ∈ s} ∈ (nhds (0:ℝ)).sets, from hr ▸ hs,
+      let ⟨l, u, hl, hu, h⟩ := (mem_nhds_lattice_unbounded (no_top 0) (no_bot 0)).mp hs in
+      have nhds (of_real r) = nhds ⊥, by simp [hr]; refl,
+      begin
+        rw [this, nhds_bot_orderable],
+        apply mem_infi_sets (of_real u) _,
+        apply mem_infi_sets (zero_lt_of_real_iff.mpr hu) _,
+        simp [set.subset_def],
+        intro x, rw [lt_iff_exists_of_real],
+        simp [le_of_lt hu] {contextual := tt},
+        exact assume p _ hp hpu, h _ (lt_of_lt_of_le hl hp) hpu
+      end)
+    (assume : r ≠ 0,
+      have hr' : 0 < r, from lt_of_le_of_ne hr this.symm,
+      have h' : map (of_ennreal ∘ of_real) (nhds r) = map id (nhds r),
+        from map_cong $ (nhds r).upwards_sets (mem_nhds_sets (is_open_lt' 0) hr') $
+          assume r hr, by simp [le_of_lt hr, (∘)],
+      le_of_map_le_map_inj' h₁ h₂ h $ le_trans (tendsto_of_ennreal hr) $ by simp [h']))
+  tendsto_of_real
+
+/- TODO
 instance : topological_add_monoid ennreal :=
 have ∀a₁ a₂ : ennreal, tendsto (λp:ennreal×ennreal, p.1 + p.2) (nhds (a₁, a₂)) (nhds (a₁ + a₂)),
   from forall_ennreal.mpr ⟨_, _⟩,
-⟨continuous_iff_tendsto.mpr $
-  assume ⟨a₁, a₂⟩,
-  begin simp [nhds_prod_eq] end⟩
+⟨continuous_iff_tendsto.mpr _⟩
 -/
 
 end topological_space

topology/topological_space.lean

@@ -117,6 +117,9 @@ lemma is_closed_imp [topological_space α] {p q : α → Prop}
 have {x | p x → q x} = (- {x | p x}) ∪ {x | q x}, from set.ext $ by finish,
 by rw [this]; exact is_closed_union (is_closed_compl_iff.mpr hp) hq
 
+lemma is_open_neg : is_closed {a | p a} → is_open {a | ¬ p a} :=
+is_open_compl_iff.mpr
+
 /- interior -/
 def interior (s : set α) : set α := ⋃₀ {t | is_open t ∧ t ⊆ s}