From 40f673ee5962d4e99573b8a8fa2a89afad573f84 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 9 Nov 2020 00:48:26 +0000
Subject: [PATCH] =?UTF-8?q?feat(data/set/intervals/pi):=20lemmas=20about?=
 =?UTF-8?q?=20intervals=20in=20`=CE=A0=20i,=20=CF=80=20i`=20(#4951)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Also add missing lemmas `Ixx_mem_nhds` and lemmas `pi_Ixx_mem_nhds`.
For each `pi_Ixx_mem_nhds` I add a non-dependent version
`pi_Ixx_mem_nhds'` because sometimes Lean fails to unify different
instances while trying to apply the dependent version to `ι → ℝ`.
---
 src/data/set/basic.lean           |  3 +
 src/data/set/intervals/pi.lean    | 67 +++++++++++++++++++++
 src/order/basic.lean              |  4 ++
 src/topology/algebra/ordered.lean | 97 +++++++++++++++++++++++++++++++
 src/topology/constructions.lean   |  5 ++
 src/topology/instances/real.lean  |  3 +
 6 files changed, 179 insertions(+)
 create mode 100644 src/data/set/intervals/pi.lean

diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 2008a2a180019..eba01851aaf5a 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2027,6 +2027,9 @@ by simp
 
 @[simp] lemma empty_pi (s : Π i, set (α i)) : pi ∅ s = univ := by { ext, simp [pi] }
 
+lemma pi_mono (h : ∀ i ∈ s, t₁ i ⊆ t₂ i) : pi s t₁ ⊆ pi s t₂ :=
+λ x hx i hi, (h i hi $ hx i hi)
+
 lemma pi_eq_empty {i : ι} (hs : i ∈ s) (ht : t i = ∅) : s.pi t = ∅ :=
 by { ext f, simp only [mem_empty_eq, not_forall, iff_false, mem_pi, not_imp],
      exact ⟨i, hs, by simp [ht]⟩ }
diff --git a/src/data/set/intervals/pi.lean b/src/data/set/intervals/pi.lean
new file mode 100644
index 0000000000000..2a45a687f7923
--- /dev/null
+++ b/src/data/set/intervals/pi.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury Kudryashov
+-/
+import data.set.intervals.basic
+import data.set.lattice
+
+/-!
+# Intervals in `pi`-space
+
+In this we prove various simple lemmas about intervals in `Π i, α i`. Closed intervals (`Ici x`,
+`Iic x`, `Icc x y`) are equal to products of their projections to `α i`, while (semi-)open intervals
+usually include the corresponding products as proper subsets.
+-/
+
+variables {ι : Type*} {α : ι → Type*}
+
+namespace set
+
+section pi_preorder
+
+variables [Π i, preorder (α i)] (x y : Π i, α i)
+
+@[simp] lemma pi_univ_Ici : pi univ (λ i, Ici (x i)) = Ici x :=
+ext $ λ y, by simp [pi.le_def]
+
+@[simp] lemma pi_univ_Iic : pi univ (λ i, Iic (x i)) = Iic x :=
+ext $ λ y, by simp [pi.le_def]
+
+@[simp] lemma pi_univ_Icc : pi univ (λ i, Icc (x i) (y i)) = Icc x y :=
+ext $ λ y, by simp [pi.le_def, forall_and_distrib]
+
+variable [nonempty ι]
+
+lemma pi_univ_Ioi_subset : pi univ (λ i, Ioi (x i)) ⊆ Ioi x :=
+λ z hz, ⟨λ i, le_of_lt $ hz i trivial,
+  λ h, nonempty.elim ‹nonempty ι› $ λ i, (h i).not_lt (hz i trivial)⟩
+
+lemma pi_univ_Iio_subset : pi univ (λ i, Iio (x i)) ⊆ Iio x :=
+@pi_univ_Ioi_subset ι (λ i, order_dual (α i)) _ x _
+
+lemma pi_univ_Ioo_subset : pi univ (λ i, Ioo (x i) (y i)) ⊆ Ioo x y :=
+λ x hx, ⟨pi_univ_Ioi_subset _ $ λ i hi, (hx i hi).1, pi_univ_Iio_subset _ $ λ i hi, (hx i hi).2⟩
+
+lemma pi_univ_Ioc_subset : pi univ (λ i, Ioc (x i) (y i)) ⊆ Ioc x y :=
+λ x hx, ⟨pi_univ_Ioi_subset _ $ λ i hi, (hx i hi).1, λ i, (hx i trivial).2⟩
+
+lemma pi_univ_Ico_subset : pi univ (λ i, Ico (x i) (y i)) ⊆ Ico x y :=
+λ x hx, ⟨λ i, (hx i trivial).1, pi_univ_Iio_subset _ $ λ i hi, (hx i hi).2⟩
+
+end pi_preorder
+
+lemma Icc_diff_pi_univ_Ioc_subset [decidable_eq ι] [Π i, linear_order (α i)] (x y z : Π i, α i) :
+  Icc x z \ pi univ (λ i, Ioc (y i) (z i)) ⊆ ⋃ i : ι, Icc x (function.update z i (y i)) :=
+begin
+  rintros a ⟨⟨hax, haz⟩, hay⟩,
+  simp only [mem_Ioc, mem_univ_pi, not_forall, not_and_distrib, not_lt] at hay,
+  rcases hay with ⟨i, hi⟩,
+  replace hi : a i ≤ y i := hi.elim id (λ h, (h $ haz i).elim),
+  refine mem_Union.2 ⟨i, ⟨hax, λ j, _⟩⟩,
+  by_cases hj : j = i,
+  { subst j, simpa },
+  { simp [hj, haz j] }
+end
+
+end set
diff --git a/src/order/basic.lean b/src/order/basic.lean
index 757e75014897d..7175f8a3d172e 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -320,6 +320,10 @@ instance pi.preorder {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)]
   le_refl  := assume a i, le_refl (a i),
   le_trans := assume a b c h₁ h₂ i, le_trans (h₁ i) (h₂ i) }
 
+lemma pi.le_def {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)] {x y : Π i, α i} :
+  x ≤ y ↔ ∀ i, x i ≤ y i :=
+iff.rfl
+
 instance pi.partial_order {ι : Type u} {α : ι → Type v} [∀i, partial_order (α i)] :
   partial_order (Πi, α i) :=
 { le_antisymm := λf g h1 h2, funext (λb, le_antisymm (h1 b) (h2 b)),
diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean
index f4dd4e608be50..1a5e6a66c40ad 100644
--- a/src/topology/algebra/ordered.lean
+++ b/src/topology/algebra/ordered.lean
@@ -12,6 +12,7 @@ import order.liminf_limsup
 import data.set.intervals.image_preimage
 import data.set.intervals.ord_connected
 import data.set.intervals.surj_on
+import data.set.intervals.pi
 import topology.algebra.group
 import topology.extend_from_subset
 import order.filter.interval
@@ -973,9 +974,105 @@ mem_nhds_sets is_open_Iio h
 lemma Ioi_mem_nhds {a b : α} (h : a < b) : Ioi a ∈ 𝓝 b :=
 mem_nhds_sets is_open_Ioi h
 
+lemma Iic_mem_nhds {a b : α} (h : a < b) : Iic b ∈ 𝓝 a :=
+mem_sets_of_superset (Iio_mem_nhds h) Iio_subset_Iic_self
+
+lemma Ici_mem_nhds {a b : α} (h : a < b) : Ici a ∈ 𝓝 b :=
+mem_sets_of_superset (Ioi_mem_nhds h) Ioi_subset_Ici_self
+
 lemma Ioo_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioo a b ∈ 𝓝 x :=
 mem_nhds_sets is_open_Ioo ⟨ha, hb⟩
 
+lemma Ioc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioc a b ∈ 𝓝 x :=
+mem_sets_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ioc_self
+
+lemma Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x :=
+mem_sets_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ico_self
+
+lemma Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x :=
+mem_sets_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self
+
+section pi
+
+/-!
+### Intervals in `Π i, π i` belong to `𝓝 x`
+
+For each leamma `pi_Ixx_mem_nhds` we add a non-dependent version `pi_Ixx_mem_nhds'` because
+sometimes Lean fails to unify different instances while trying to apply the dependent version to,
+e.g., `ι → ℝ`.
+-/
+
+variables {ι : Type*} {π : ι → Type*} [fintype ι] [Π i, linear_order (π i)]
+  [Π i, topological_space (π i)] [∀ i, order_topology (π i)] {a b x : Π i, π i} {a' b' x' : ι → α}
+
+lemma pi_Iic_mem_nhds (ha : ∀ i, x i < a i) : Iic a ∈ 𝓝 x :=
+pi_univ_Iic a ▸ set_pi_mem_nhds (finite.of_fintype _) (λ i _, Iic_mem_nhds (ha _))
+
+lemma pi_Iic_mem_nhds' (ha : ∀ i, x' i < a' i) : Iic a' ∈ 𝓝 x' :=
+pi_Iic_mem_nhds ha
+
+lemma pi_Ici_mem_nhds (ha : ∀ i, a i < x i) : Ici a ∈ 𝓝 x :=
+pi_univ_Ici a ▸ set_pi_mem_nhds (finite.of_fintype _) (λ i _, Ici_mem_nhds (ha _))
+
+lemma pi_Ici_mem_nhds' (ha : ∀ i, a' i < x' i) : Ici a' ∈ 𝓝 x' :=
+pi_Ici_mem_nhds ha
+
+lemma pi_Icc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Icc a b ∈ 𝓝 x :=
+pi_univ_Icc a b ▸ set_pi_mem_nhds (finite.of_fintype _) (λ i _, Icc_mem_nhds (ha _) (hb _))
+
+lemma pi_Icc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Icc a' b' ∈ 𝓝 x' :=
+pi_Icc_mem_nhds ha hb
+
+variables [nonempty ι]
+
+lemma pi_Iio_mem_nhds (ha : ∀ i, x i < a i) : Iio a ∈ 𝓝 x :=
+begin
+  refine mem_sets_of_superset (set_pi_mem_nhds (finite.of_fintype _) (λ i _, _))
+    (pi_univ_Iio_subset a),
+  exact Iio_mem_nhds (ha i)
+end
+
+lemma pi_Iio_mem_nhds' (ha : ∀ i, x' i < a' i) : Iio a' ∈ 𝓝 x' :=
+pi_Iio_mem_nhds ha
+
+lemma pi_Ioi_mem_nhds (ha : ∀ i, a i < x i) : Ioi a ∈ 𝓝 x :=
+@pi_Iio_mem_nhds ι (λ i, order_dual (π i)) _ _ _ _ _ _ _ ha
+
+lemma pi_Ioi_mem_nhds' (ha : ∀ i, a' i < x' i) : Ioi a' ∈ 𝓝 x' :=
+pi_Ioi_mem_nhds ha
+
+lemma pi_Ioc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioc a b ∈ 𝓝 x :=
+begin
+  refine mem_sets_of_superset (set_pi_mem_nhds (finite.of_fintype _) (λ i _, _))
+    (pi_univ_Ioc_subset a b),
+  exact Ioc_mem_nhds (ha i) (hb i)
+end
+
+lemma pi_Ioc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioc a' b' ∈ 𝓝 x' :=
+pi_Ioc_mem_nhds ha hb
+
+lemma pi_Ico_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ico a b ∈ 𝓝 x :=
+begin
+  refine mem_sets_of_superset (set_pi_mem_nhds (finite.of_fintype _) (λ i _, _))
+    (pi_univ_Ico_subset a b),
+  exact Ico_mem_nhds (ha i) (hb i)
+end
+
+lemma pi_Ico_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ico a' b' ∈ 𝓝 x' :=
+pi_Ico_mem_nhds ha hb
+
+lemma pi_Ioo_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioo a b ∈ 𝓝 x :=
+begin
+  refine mem_sets_of_superset (set_pi_mem_nhds (finite.of_fintype _) (λ i _, _))
+    (pi_univ_Ioo_subset a b),
+  exact Ioo_mem_nhds (ha i) (hb i)
+end
+
+lemma pi_Ioo_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioo a' b' ∈ 𝓝 x' :=
+pi_Ioo_mem_nhds ha hb
+
+end pi
+
 lemma disjoint_nhds_at_top [no_top_order α] (x : α) :
   disjoint (𝓝 x) at_top :=
 begin
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index 7bb032076578b..68535e2b24f3b 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -604,6 +604,11 @@ lemma is_open_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set
   (hi : finite i) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) :=
 by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, continuous_apply a _ $ hs a ha)
 
+lemma set_pi_mem_nhds [Π a, topological_space (π a)] {i : set ι} {s : Π a, set (π a)}
+  {x : Π a, π a} (hi : finite i) (hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)) :
+  pi i s ∈ 𝓝 x :=
+by { rw [pi_def], exact Inter_mem_sets hi (λ a ha, (continuous_apply a).continuous_at (hs a ha)) }
+
 lemma pi_eq_generate_from [∀a, topological_space (π a)] :
   Pi.topological_space =
   generate_from {g | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, is_open (s a)) ∧ g = pi ↑i s} :=
diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean
index 673ba3898a761..1c79a1d3029c7 100644
--- a/src/topology/instances/real.lean
+++ b/src/topology/instances/real.lean
@@ -294,6 +294,9 @@ compact_of_totally_bounded_is_closed
   (real.totally_bounded_Icc a b)
   (is_closed_inter (is_closed_ge' a) (is_closed_le' b))
 
+lemma compact_pi_Icc {ι : Type*} {a b : ι → ℝ} : is_compact (Icc a b) :=
+pi_univ_Icc a b ▸ compact_univ_pi $ λ i, compact_Icc
+
 instance : proper_space ℝ :=
 { compact_ball := λx r, by rw closed_ball_Icc; apply compact_Icc }