feat(data/set/basic): more lemmas about set.pi (#5603)

src/data/pi.lean

@@ -28,6 +28,8 @@ namespace pi
 ⟨λ _, 1⟩
 @[simp, to_additive] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
 
+@[to_additive] lemma one_def [Π i, has_one $ f i] : (1 : Π i, f i) = λ i, 1 := rfl
+
 @[to_additive]
 instance has_mul [∀ i, has_mul $ f i] :
   has_mul (Π i : I, f i) :=

src/data/set/basic.lean

@@ -2091,7 +2091,7 @@ end prod
 /-! ### Lemmas about set-indexed products of sets -/
 
 section pi
-variables {ι : Type*} {α : ι → Type*} {s : set ι} {t t₁ t₂ : Π i, set (α i)}
+variables {ι : Type*} {α : ι → Type*} {s s₁ : set ι} {t t₁ t₂ : Π i, set (α i)}
 
 /-- Given an index set `i` and a family of sets `s : Π i, set (α i)`, `pi i s`
 is the set of dependent functions `f : Πa, π a` such that `f a` belongs to `π a`
@@ -2106,9 +2106,15 @@ by simp
 
 @[simp] lemma empty_pi (s : Π i, set (α i)) : pi ∅ s = univ := by { ext, simp [pi] }
 
+@[simp] lemma pi_univ (s : set ι) : pi s (λ i, (univ : set (α i))) = univ :=
+eq_univ_of_forall $ λ f i hi, mem_univ _
+
 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_congr (h : s = s₁) (h' : ∀ i ∈ s, t i = t₁ i) : pi s t = pi s₁ t₁ :=
+h ▸ (ext $ λ x, forall_congr $ λ i, forall_congr $ λ hi, h' i hi ▸ iff.rfl)
+
 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]⟩ }
@@ -2143,6 +2149,9 @@ by { ext, simp [pi, or_imp_distrib, forall_and_distrib] }
   pi {i} t = (eval i ⁻¹' t i) :=
 by { ext, simp [pi] }
 
+lemma singleton_pi' (i : ι) (t : Π i, set (α i)) : pi {i} t = {x | x i ∈ t i} :=
+singleton_pi i t
+
 lemma pi_if {p : ι → Prop} [h : decidable_pred p] (s : set ι) (t₁ t₂ : Π i, set (α i)) :
   pi s (λ i, if p i then t₁ i else t₂ i) = pi {i ∈ s | p i} t₁ ∩ pi {i ∈ s | ¬ p i} t₂ :=
 begin
@@ -2153,6 +2162,34 @@ begin
     by_cases p i; simp * at * }
 end
 
+lemma union_pi : (s ∪ s₁).pi t = s.pi t ∩ s₁.pi t :=
+by simp [pi, or_imp_distrib, forall_and_distrib, set_of_and]
+
+@[simp] lemma pi_inter_compl (s : set ι) : pi s t ∩ pi sᶜ t = pi univ t :=
+by rw [← union_pi, union_compl_self]
+
+lemma pi_update_of_not_mem [decidable_eq ι] {β : Π i, Type*} {i : ι} (hi : i ∉ s) (f : Π j, α j)
+  (a : α i) (t : Π j, α j → set (β j)) :
+  s.pi (λ j, t j (update f i a j)) = s.pi (λ j, t j (f j)) :=
+pi_congr rfl $ λ j hj, by { rw update_noteq, exact λ h, hi (h ▸ hj) }
+
+lemma pi_update_of_mem [decidable_eq ι] {β : Π i, Type*} {i : ι} (hi : i ∈ s) (f : Π j, α j)
+  (a : α i) (t : Π j, α j → set (β j)) :
+  s.pi (λ j, t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi (λ j, t j (f j)) :=
+calc s.pi (λ j, t j (update f i a j)) = ({i} ∪ s \ {i}).pi (λ j, t j (update f i a j)) :
+  by rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]
+... = {x | x i ∈ t i a} ∩ (s \ {i}).pi (λ j, t j (f j)) :
+  by { rw [union_pi, singleton_pi', update_same, pi_update_of_not_mem], simp }
+
+lemma univ_pi_update [decidable_eq ι] {β : Π i, Type*} (i : ι) (f : Π j, α j)
+  (a : α i) (t : Π j, α j → set (β j)) :
+  pi univ (λ j, t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi {i}ᶜ (λ j, t j (f j)) :=
+by rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]
+
+lemma univ_pi_update_univ [decidable_eq ι] (i : ι) (s : set (α i)) :
+  pi univ (update (λ j : ι, (univ : set (α j))) i s) = eval i ⁻¹' s :=
+by rw [univ_pi_update i (λ j, (univ : set (α j))) s (λ j t, t), pi_univ, inter_univ, preimage]
+
 open_locale classical
 
 lemma eval_image_pi {i : ι} (hs : i ∈ s) (ht : (s.pi t).nonempty) : eval i '' s.pi t = t i :=

src/data/set/intervals/pi.lean

@@ -31,6 +31,8 @@ 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]
 
+section nonempty
+
 variable [nonempty ι]
 
 lemma pi_univ_Ioi_subset : pi univ (λ i, Ioi (x i)) ⊆ Ioi x :=
@@ -49,12 +51,55 @@ lemma pi_univ_Ioc_subset : pi univ (λ i, Ioc (x i) (y i)) ⊆ Ioc x y :=
 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 nonempty
+
+variable [decidable_eq ι]
+
+open function (update)
+
+lemma pi_univ_Ioc_update_left {x y : Π i, α i} {i₀ : ι} {m : α i₀} (hm : x i₀ ≤ m) :
+  pi univ (λ i, Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ pi univ (λ i, Ioc (x i) (y i)) :=
+begin
+  have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀),
+    by rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
+      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)],
+  simp_rw [univ_pi_update i₀ _ _ (λ i z, Ioc z (y i)), ← pi_inter_compl ({i₀} : set ι),
+    singleton_pi', ← inter_assoc, this],
+  refl
+end
+
+lemma pi_univ_Ioc_update_right {x y : Π i, α i} {i₀ : ι} {m : α i₀} (hm : m ≤ y i₀) :
+  pi univ (λ i, Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ (λ i, Ioc (x i) (y i)) :=
+begin
+  have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀),
+    by rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
+      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)],
+  simp_rw [univ_pi_update i₀ y m (λ i z, Ioc (x i) z), ← pi_inter_compl ({i₀} : set ι),
+    singleton_pi', ← inter_assoc, this],
+  refl
+end
+
+lemma disjoint_pi_univ_Ioc_update_left_right {x y : Π i, α i} {i₀ : ι} {m : α i₀} :
+  disjoint (pi univ (λ i, Ioc (x i) (update y i₀ m i)))
+    (pi univ (λ i, Ioc (update x i₀ m i) (y i))) :=
+begin
+  rintro z ⟨h₁, h₂⟩,
+  refine (h₁ i₀ (mem_univ _)).2.not_lt _,
+  simpa only [function.update_same] using (h₂ i₀ (mem_univ _)).1
+end
+
 end pi_preorder
 
 variables [decidable_eq ι] [Π i, linear_order (α i)]
 
 open function (update)
 
+lemma pi_univ_Ioc_update_union (x y : Π i, α i) (i₀ : ι) (m : α i₀) (hm : m ∈ Icc (x i₀) (y i₀)) :
+  pi univ (λ i, Ioc (x i) (update y i₀ m i)) ∪ pi univ (λ i, Ioc (update x i₀ m i) (y i)) =
+    pi univ (λ i, Ioc (x i) (y i)) :=
+by simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2,
+  ← union_inter_distrib_right, ← set_of_or, le_or_lt, set_of_true, univ_inter]
+
 /-- If `x`, `y`, `x'`, and `y'` are functions `Π i : ι, α i`, then
 the set difference between the box `[x, y]` and the product of the open intervals `(x' i, y' i)`
 is covered by the union of the following boxes: for each `i : ι`, we take