feat(*): random lemmas about sets and filters (#3118)

This is the first in a series of PR that will culminate in a proof of Heine's theorem (a continuous function from a compact separated uniform space to any uniform space is uniformly continuous). I'm slicing a 600 lines files into PRs. This first PR is only about sets, filters and a bit of topology. Uniform spaces stuff will come later.




Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: PatrickMassot

src/data/set/basic.lean

@@ -340,6 +340,9 @@ lemma exists_mem_of_nonempty (α) : ∀ [nonempty α], ∃x:α, x ∈ (univ : se
 instance univ_decidable : decidable_pred (@set.univ α) :=
 λ x, is_true trivial
 
+/-- `diagonal α` is the subset of `α × α` consisting of all pairs of the form `(a, a)`. -/
+def diagonal (α : Type*) : set (α × α) := {p | p.1 = p.2}
+
 /-! ### Lemmas about union -/
 
 theorem union_def {s₁ s₂ : set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂} := rfl
@@ -495,6 +498,16 @@ by finish [subset_def, ext_iff, iff_def]
 theorem inter_eq_self_of_subset_right {s t : set α} (h : t ⊆ s) : s ∩ t = t :=
 by finish [subset_def, ext_iff, iff_def]
 
+lemma inter_compl_nonempty_iff {α : Type*} {s t : set α} : (s ∩ -t).nonempty ↔ ¬ s ⊆ t :=
+begin
+  split,
+  { rintros ⟨x ,xs, xt⟩ sub,
+    exact xt (sub xs) },
+  { intros h,
+    rcases not_subset.mp h with ⟨x, xs, xt⟩,
+    exact ⟨x, xs, xt⟩ }
+end
+
 theorem union_inter_cancel_left {s t : set α} : (s ∪ t) ∩ s = s :=
 by finish [ext_iff, iff_def]
 
@@ -987,6 +1000,13 @@ begin
   simp [mem_def, h]
 end
 
+lemma preimage_coe_coe_diagonal {α : Type*} (s : set α) :
+  (prod.map coe coe) ⁻¹' (diagonal α) = diagonal s :=
+begin
+  ext ⟨⟨x, x_in⟩, ⟨y, y_in⟩⟩,
+  simp [set.diagonal],
+end
+
 end preimage
 
 /-! ### Image of a set under a function -/
@@ -1508,6 +1528,7 @@ begin
   rintro ⟨s, hs₁, hs₂⟩, refine ⟨subtype.val ⁻¹' s, _⟩,
   rw [image_preimage_eq_of_subset], exact hs₂, rw [range_val], exact hs₁
 end
+
 end subtype
 
 namespace set

src/order/filter/bases.lean

@@ -249,6 +249,22 @@ lemma has_basis.forall_nonempty_iff_ne_bot (hl : l.has_basis p s) :
 lemma basis_sets (l : filter α) : l.has_basis (λ s : set α, s ∈ l) id :=
 ⟨λ t, exists_sets_subset_iff.symm⟩
 
+lemma has_basis_self {l : filter α} {P : set α → Prop} :
+  has_basis l (λ s, s ∈ l ∧ P s) id ↔ ∀ t, (t ∈ l ↔ ∃ r ∈ l, P r ∧ r ⊆ t) :=
+begin
+  split,
+  { rintros ⟨h⟩ t,
+    convert h t,
+    ext s,
+    tauto, },
+  { intro h,
+    constructor,
+    intro t,
+    convert h t,
+    ext s,
+    tauto }
+end
+
 lemma at_top_basis [nonempty α] [semilattice_sup α] :
   (@at_top α _).has_basis (λ _, true) Ici :=
 ⟨λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t⟩
@@ -331,6 +347,10 @@ lemma has_basis.comap (f : β → α) (hl : l.has_basis p s) :
     exact ⟨s i, ⟨i, hi, subset.refl _⟩, H⟩ }
 end⟩
 
+lemma comap_has_basis (f : α → β) (l : filter β) :
+  has_basis (comap f l) (λ s : set β, s ∈ l) (λ s, f ⁻¹' s) :=
+⟨λ t, mem_comap_sets⟩
+
 lemma has_basis.prod_self (hl : l.has_basis p s) :
   (l.prod l).has_basis p (λ i, (s i).prod (s i)) :=
 ⟨begin
@@ -356,6 +376,20 @@ lemma has_basis.forall_iff (hl : l.has_basis p s) {P : set α → Prop}
 ⟨λ H i hi, H (s i) $ hl.mem_of_mem hi,
   λ H s hs, let ⟨i, hi, his⟩ := hl.mem_iff.1 hs in mono his (H i hi)⟩
 
+lemma has_basis.sInter_sets (h : has_basis l p s) :
+  ⋂₀ l.sets = ⋂ i ∈ set_of p, s i :=
+begin
+  ext x,
+  suffices : (∀ t ∈ l, x ∈ t) ↔ ∀ i, p i → x ∈ s i,
+    by simpa only [mem_Inter, mem_set_of_eq, mem_sInter],
+  simp_rw h.mem_iff,
+  split,
+  { intros h i hi,
+    exact h (s i) ⟨i, hi, subset.refl _⟩ },
+  { rintros h _ ⟨i, hi, sub⟩,
+    exact sub (h i hi) },
+end
+
 variables [preorder ι] (l p s)
 
 /-- `is_antimono_basis p s` means the image of `s` bounded by `p` is a filter basis
@@ -408,6 +442,28 @@ lemma has_basis.prod (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
   (la.prod lb).has_basis (λ i : ι × ι', pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) :=
 (hla.comap prod.fst).inf (hlb.comap prod.snd)
 
+lemma has_basis.prod' {la : filter α} {lb : filter β} {ι : Type*} {p : ι → Prop}
+  {sa : ι → set α} {sb : ι → set β}
+  (hla : la.has_basis p sa) (hlb : lb.has_basis p sb)
+  (h_dir : ∀ {i j}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) :
+  (la.prod lb).has_basis p (λ i, (sa i).prod (sb i)) :=
+⟨begin
+  intros t,
+  rw mem_prod_iff,
+  split,
+  { rintros ⟨u, u_in, v, v_in, huv⟩,
+    rcases hla.mem_iff.mp u_in with ⟨i, hi, si⟩,
+    rcases hlb.mem_iff.mp v_in with ⟨j, hj, sj⟩,
+    rcases h_dir hi hj with ⟨k, hk, ki, kj⟩,
+    use [k, hk],
+    calc
+    (sa k).prod (sb k) ⊆ (sa i).prod (sb j) : set.prod_mono ki kj
+                   ... ⊆ u.prod v           : set.prod_mono si sj
+                   ... ⊆ t                  : huv, },
+  { rintro ⟨i, hi, h⟩,
+    exact ⟨sa i, hla.mem_of_mem hi, sb i, hlb.mem_of_mem hi, h⟩ },
+end⟩
+
 lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α}
   {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α}
   (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l  :=

src/order/filter/basic.lean

@@ -487,6 +487,21 @@ begin
     use [a, hUV ha] }
 end
 
+lemma inf_principal_ne_bot_iff (f : filter α) (s : set α) :
+  f ⊓ principal s ≠ ⊥ ↔ ∀ U ∈ f, (U ∩ s).nonempty :=
+begin
+  rw inf_ne_bot_iff,
+  apply forall_congr,
+  intros U,
+  split,
+  { intros h U_in,
+    exact h U_in (mem_principal_self s) },
+  { intros h V U_in V_in,
+    rw mem_principal_sets at V_in,
+    cases h U_in with x hx,
+    exact ⟨x, hx.1, V_in hx.2⟩ },
+end
+
 lemma inf_eq_bot_iff {f g : filter α} :
   f ⊓ g = ⊥ ↔ ∃ U V, (U ∈ f) ∧ (V ∈ g) ∧ U ∩ V = ∅ :=
 begin
@@ -1291,6 +1306,22 @@ theorem map_comap_of_surjective {f : α → β} (hf : function.surjective f) (l
   map f (comap f l) = l :=
 le_antisymm map_comap_le (le_map_comap_of_surjective hf l)
 
+lemma subtype_coe_map_comap (s : set α) (f : filter α) :
+  map (coe : s → α) (comap (coe : s → α) f) = f ⊓ principal s :=
+begin
+  apply le_antisymm,
+  { rw [map_le_iff_le_comap, comap_inf, comap_principal],
+    have : (coe : s → α) ⁻¹' s = univ, by { ext x, simp },
+    rw [this, principal_univ],
+    simp [le_refl _] },
+  { intros V V_in,
+    rcases V_in with ⟨W, W_in, H⟩,
+    rw mem_inf_sets,
+    use [W, W_in, s, mem_principal_self s],
+    erw [← image_subset_iff, subtype.image_preimage_val] at H,
+    exact H }
+end
+
 lemma comap_ne_bot {f : filter β} {m : α → β} (hm : ∀t∈ f, ∃a, m a ∈ t) :
   comap m f ≠ ⊥ :=
 forall_sets_nonempty_iff_ne_bot.mp $ assume s ⟨t, ht, t_s⟩,
@@ -1893,6 +1924,14 @@ le_antisymm
         ... ⊆ _ : by rwa [image_subset_iff])
   ((tendsto.comp (le_refl _) tendsto_fst).prod_mk (tendsto.comp (le_refl _) tendsto_snd))
 
+lemma tendsto.prod_map {δ : Type*} {f : α → γ} {g : β → δ} {a : filter α} {b : filter β}
+  {c : filter γ} {d : filter δ} (hf : tendsto f a c) (hg : tendsto g b d) :
+  tendsto (prod.map f g) (a ×ᶠ b) (c ×ᶠ d) :=
+begin
+  erw [tendsto, ← prod_map_map_eq],
+  exact filter.prod_mono hf hg,
+end
+
 lemma map_prod (m : α × β → γ) (f : filter α) (g : filter β) :
   map m (f.prod g) = (f.map (λa b, m (a, b))).seq g :=
 begin

src/topology/algebra/ordered.lean

@@ -193,12 +193,7 @@ then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/
 lemma is_closed.is_closed_le [topological_space β] {f g : β → α} {s : set β} (hs : is_closed s)
   (hf : continuous_on f s) (hg : continuous_on g s) :
   is_closed {x ∈ s | f x ≤ g x} :=
-begin
-  have A : {x ∈ s | f x ≤ g x} ⊆ s := inter_subset_left _ _,
-  refine is_closed_of_closure_subset (λ x hx, _),
-  have B : x ∈ s := closure_minimal A hs hx,
-  exact ⟨B, ((hf x B).mono A).closure_le hx ((hg x B).mono A) (λ y, and.right)⟩
-end
+(hf.prod hg).preimage_closed_of_closed hs order_closed_topology.is_closed_le'
 
 end preorder
 

src/topology/continuous_on.lean

@@ -23,7 +23,7 @@ equipped with the subspace topology.
 open set filter
 open_locale topological_space
 
-variables {α : Type*} {β : Type*} {γ : Type*}
+variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 variables [topological_space α]
 
 /-- The "neighborhood within" filter. Elements of `nhds_within a s` are sets containing the
@@ -205,7 +205,7 @@ theorem tendsto_nhds_within_iff_subtype {s : set α} {a : α} (h : a ∈ s) (f :
   tendsto f (nhds_within a s) l ↔ tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l :=
 by { simp only [tendsto, nhds_within_eq_map_subtype_val h, filter.map_map], refl }
 
-variables [topological_space β] [topological_space γ]
+variables [topological_space β] [topological_space γ] [topological_space δ]
 
 /-- A function between topological spaces is continuous at a point `x₀` within a subset `s`
 if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. -/
@@ -241,6 +241,16 @@ tendsto_inf.2 ⟨h, tendsto_principal.2 $
   mem_inf_sets_of_right $ mem_principal_sets.2 $
   λ x, mem_image_of_mem _⟩
 
+lemma continuous_within_at.prod_map {f : α → γ} {g : β → δ} {s : set α} {t : set β}
+  {x : α} {y : β}
+  (hf : continuous_within_at f s x) (hg : continuous_within_at g t y) :
+  continuous_within_at (prod.map f g) (s.prod t) (x, y) :=
+begin
+  unfold continuous_within_at at *,
+  rw [nhds_within_prod_eq, prod.map, nhds_prod_eq],
+  exact hf.prod_map hg,
+end
+
 theorem continuous_on_iff {f : α → β} {s : set α} :
   continuous_on f s ↔ ∀ x ∈ s, ∀ t : set β, is_open t → f x ∈ t → ∃ u, is_open u ∧ x ∈ u ∧
     u ∩ s ⊆ f ⁻¹' t :=
@@ -277,6 +287,11 @@ have ∀ t, is_closed (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_closed u
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous_iff_is_closed]; simp only [this]
 
+lemma continuous_on.prod_map {f : α → γ} {g : β → δ} {s : set α} {t : set β}
+  (hf : continuous_on f s) (hg : continuous_on g t) :
+  continuous_on (prod.map f g) (s.prod t) :=
+λ ⟨x, y⟩ ⟨hx, hy⟩, continuous_within_at.prod_map (hf x hx) (hg y hy)
+
 lemma continuous_on_empty (f : α → β) : continuous_on f ∅ :=
 λ x, false.elim