Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 9437902

Browse files
urkudurkud
committed
refactor(data/set/pointwise/interval): split (#17873)
* Extract `data.set.interval.monoid` from `data.set.pointwise.interval`. * Import it in `data.finset.locally_finite`, golf some proofs. * Add `finset.map_add_left_Icc` etc.
1 parent b16045e commit 9437902

File tree

4 files changed

+170
-173
lines changed

4 files changed

+170
-173
lines changed

‎src/algebra/big_operators/intervals.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,7 @@ variables [comm_monoid β]
3232
lemma prod_Ico_add' [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α]
3333
[locally_finite_order α] (f : α → β) (a b c : α) :
3434
(∏ x in Ico a b, f (x + c)) = (∏ x in Ico (a + c) (b + c), f x) :=
35-
begin
36-
classical,
37-
rw [←image_add_right_Ico, prod_image (λ x hx y hy h, add_right_cancel h)],
38-
end
35+
by { rw [← map_add_right_Ico, prod_map], refl }
3936

4037
@[to_additive]
4138
lemma prod_Ico_add [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α]

‎src/data/finset/locally_finite.lean‎

Lines changed: 49 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison, Yaël Dillies
55
-/
66
import order.locally_finite
7+
import data.set.intervals.monoid
78

89
/-!
910
# Intervals as finsets
@@ -498,78 +499,65 @@ by { ext, simp [eq_comm] }
498499
end linear_order
499500

500501
section ordered_cancel_add_comm_monoid
501-
variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] [decidable_eq α]
502-
[locally_finite_order α]
502+
variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] [locally_finite_order α]
503503

504-
lemma image_add_left_Icc (a b c : α) : (Icc a b).image ((+) c) = Icc (c + a) (c + b) :=
505-
begin
506-
ext x,
507-
rw [mem_image, mem_Icc],
508-
split,
509-
{ rintro ⟨y, hy, rfl⟩,
510-
rw mem_Icc at hy,
511-
exact ⟨add_le_add_left hy.1 c, add_le_add_left hy.2 c⟩ },
512-
{ intro hx,
513-
obtain ⟨y, hy⟩ := exists_add_of_le hx.1,
514-
rw add_assoc at hy,
515-
rw hy at hx,
516-
exact ⟨a + y, mem_Icc.2 ⟨le_of_add_le_add_left hx.1, le_of_add_le_add_left hx.2⟩, hy.symm⟩ }
517-
end
504+
@[simp] lemma map_add_left_Icc (a b c : α) :
505+
(Icc a b).map (add_left_embedding c) = Icc (c + a) (c + b) :=
506+
by { rw [← coe_inj, coe_map, coe_Icc, coe_Icc], exact set.image_const_add_Icc _ _ _ }
518507

519-
lemma image_add_left_Ico (a b c : α) : (Ico a b).image ((+) c) = Ico (c + a) (c + b) :=
520-
begin
521-
ext x,
522-
rw [mem_image, mem_Ico],
523-
split,
524-
{ rintro ⟨y, hy, rfl⟩,
525-
rw mem_Ico at hy,
526-
exact ⟨add_le_add_left hy.1 c, add_lt_add_left hy.2 c⟩ },
527-
{ intro hx,
528-
obtain ⟨y, hy⟩ := exists_add_of_le hx.1,
529-
rw add_assoc at hy,
530-
rw hy at hx,
531-
exact ⟨a + y, mem_Ico.2 ⟨le_of_add_le_add_left hx.1, lt_of_add_lt_add_left hx.2⟩, hy.symm⟩ }
532-
end
508+
@[simp] lemma map_add_right_Icc (a b c : α) :
509+
(Icc a b).map (add_right_embedding c) = Icc (a + c) (b + c) :=
510+
by { rw [← coe_inj, coe_map, coe_Icc, coe_Icc], exact set.image_add_const_Icc _ _ _ }
533511

534-
lemma image_add_left_Ioc (a b c : α) : (Ioc a b).image ((+) c) = Ioc (c + a) (c + b) :=
535-
begin
536-
ext x,
537-
rw [mem_image, mem_Ioc],
538-
refine ⟨_, λ hx, _⟩,
539-
{ rintro ⟨y, hy, rfl⟩,
540-
rw mem_Ioc at hy,
541-
exact ⟨add_lt_add_left hy.1 c, add_le_add_left hy.2 c⟩ },
542-
{ obtain ⟨y, hy⟩ := exists_add_of_le hx.1.le,
543-
rw add_assoc at hy,
544-
rw hy at hx,
545-
exact ⟨a + y, mem_Ioc.2 ⟨lt_of_add_lt_add_left hx.1, le_of_add_le_add_left hx.2⟩, hy.symm⟩ }
546-
end
512+
@[simp] lemma map_add_left_Ico (a b c : α) :
513+
(Ico a b).map (add_left_embedding c) = Ico (c + a) (c + b) :=
514+
by { rw [← coe_inj, coe_map, coe_Ico, coe_Ico], exact set.image_const_add_Ico _ _ _ }
547515

548-
lemma image_add_left_Ioo (a b c : α) : (Ioo a b).image ((+) c) = Ioo (c + a) (c + b) :=
549-
begin
550-
ext x,
551-
rw [mem_image, mem_Ioo],
552-
refine ⟨_, λ hx, _⟩,
553-
{ rintro ⟨y, hy, rfl⟩,
554-
rw mem_Ioo at hy,
555-
exact ⟨add_lt_add_left hy.1 c, add_lt_add_left hy.2 c⟩ },
556-
{ obtain ⟨y, hy⟩ := exists_add_of_le hx.1.le,
557-
rw add_assoc at hy,
558-
rw hy at hx,
559-
exact ⟨a + y, mem_Ioo.2 ⟨lt_of_add_lt_add_left hx.1, lt_of_add_lt_add_left hx.2⟩, hy.symm⟩ }
560-
end
516+
@[simp] lemma map_add_right_Ico (a b c : α) :
517+
(Ico a b).map (add_right_embedding c) = Ico (a + c) (b + c) :=
518+
by { rw [← coe_inj, coe_map, coe_Ico, coe_Ico], exact set.image_add_const_Ico _ _ _ }
519+
520+
@[simp] lemma map_add_left_Ioc (a b c : α) :
521+
(Ioc a b).map (add_left_embedding c) = Ioc (c + a) (c + b) :=
522+
by { rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc], exact set.image_const_add_Ioc _ _ _ }
523+
524+
@[simp] lemma map_add_right_Ioc (a b c : α) :
525+
(Ioc a b).map (add_right_embedding c) = Ioc (a + c) (b + c) :=
526+
by { rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc], exact set.image_add_const_Ioc _ _ _ }
527+
528+
@[simp] lemma map_add_left_Ioo (a b c : α) :
529+
(Ioo a b).map (add_left_embedding c) = Ioo (c + a) (c + b) :=
530+
by { rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo], exact set.image_const_add_Ioo _ _ _ }
531+
532+
@[simp] lemma map_add_right_Ioo (a b c : α) :
533+
(Ioo a b).map (add_right_embedding c) = Ioo (a + c) (b + c) :=
534+
by { rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo], exact set.image_add_const_Ioo _ _ _ }
535+
536+
variables [decidable_eq α]
537+
538+
@[simp] lemma image_add_left_Icc (a b c : α) : (Icc a b).image ((+) c) = Icc (c + a) (c + b) :=
539+
by { rw [← map_add_left_Icc, map_eq_image], refl }
540+
541+
@[simp] lemma image_add_left_Ico (a b c : α) : (Ico a b).image ((+) c) = Ico (c + a) (c + b) :=
542+
by { rw [← map_add_left_Ico, map_eq_image], refl }
543+
544+
@[simp] lemma image_add_left_Ioc (a b c : α) : (Ioc a b).image ((+) c) = Ioc (c + a) (c + b) :=
545+
by { rw [← map_add_left_Ioc, map_eq_image], refl }
546+
547+
@[simp] lemma image_add_left_Ioo (a b c : α) : (Ioo a b).image ((+) c) = Ioo (c + a) (c + b) :=
548+
by { rw [← map_add_left_Ioo, map_eq_image], refl }
561549

562-
lemma image_add_right_Icc (a b c : α) : (Icc a b).image (+ c) = Icc (a + c) (b + c) :=
563-
by { simp_rw add_comm _ c, exact image_add_left_Icc a b c }
550+
@[simp] lemma image_add_right_Icc (a b c : α) : (Icc a b).image (+ c) = Icc (a + c) (b + c) :=
551+
by { rw [← map_add_right_Icc, map_eq_image], refl }
564552

565553
lemma image_add_right_Ico (a b c : α) : (Ico a b).image (+ c) = Ico (a + c) (b + c) :=
566-
by { simp_rw add_comm _ c, exact image_add_left_Ico a b c }
554+
by { rw [← map_add_right_Ico, map_eq_image], refl }
567555

568556
lemma image_add_right_Ioc (a b c : α) : (Ioc a b).image (+ c) = Ioc (a + c) (b + c) :=
569-
by { simp_rw add_comm _ c, exact image_add_left_Ioc a b c }
557+
by { rw [← map_add_right_Ioc, map_eq_image], refl }
570558

571559
lemma image_add_right_Ioo (a b c : α) : (Ioo a b).image (+ c) = Ioo (a + c) (b + c) :=
572-
by { simp_rw add_comm _ c, exact image_add_left_Ioo a b c }
560+
by { rw [← map_add_right_Ioo, map_eq_image], refl }
573561

574562
end ordered_cancel_add_comm_monoid
575563

‎src/data/set/intervals/monoid.lean‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
/-
2+
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury G. Kudryashov, Patrick Massot
5+
-/
6+
import data.set.intervals.basic
7+
import data.set.function
8+
import algebra.order.monoid.cancel.defs
9+
import algebra.order.monoid.canonical.defs
10+
import algebra.group.basic
11+
12+
/-!
13+
# Images of intervals under `(+ d)`
14+
15+
The lemmas in this file state that addition maps intervals bijectively. The typeclass
16+
`has_exists_add_of_le` is defined specifically to make them work when combined with
17+
`ordered_cancel_add_comm_monoid`; the lemmas below therefore apply to all
18+
`ordered_add_comm_group`, but also to `ℕ` and `ℝ≥0`, which are not groups.
19+
-/
20+
21+
namespace set
22+
23+
variables {M : Type*} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c d : M)
24+
25+
lemma Ici_add_bij : bij_on (+d) (Ici a) (Ici (a + d)) :=
26+
begin
27+
refine ⟨λ x h, add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).inj_on _, λ _ h, _⟩,
28+
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h),
29+
rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h,
30+
exact ⟨a + c, h, by rw add_right_comm⟩,
31+
end
32+
33+
lemma Ioi_add_bij : bij_on (+d) (Ioi a) (Ioi (a + d)) :=
34+
begin
35+
refine ⟨λ x h, add_lt_add_right (mem_Ioi.mp h) _, λ _ _ _ _ h, add_right_cancel h, λ _ h, _⟩,
36+
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le,
37+
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h,
38+
exact ⟨a + c, h, by rw add_right_comm⟩,
39+
end
40+
41+
lemma Icc_add_bij : bij_on (+d) (Icc a b) (Icc (a + d) (b + d)) :=
42+
begin
43+
rw [← Ici_inter_Iic, ← Ici_inter_Iic],
44+
exact (Ici_add_bij a d).inter_maps_to (λ x hx, add_le_add_right hx _)
45+
(λ x hx, le_of_add_le_add_right hx.2)
46+
end
47+
48+
lemma Ioo_add_bij : bij_on (+d) (Ioo a b) (Ioo (a + d) (b + d)) :=
49+
begin
50+
rw [← Ioi_inter_Iio, ← Ioi_inter_Iio],
51+
exact (Ioi_add_bij a d).inter_maps_to (λ x hx, add_lt_add_right hx _)
52+
(λ x hx, lt_of_add_lt_add_right hx.2)
53+
end
54+
55+
lemma Ioc_add_bij : bij_on (+d) (Ioc a b) (Ioc (a + d) (b + d)) :=
56+
begin
57+
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic],
58+
exact (Ioi_add_bij a d).inter_maps_to (λ x hx, add_le_add_right hx _)
59+
(λ x hx, le_of_add_le_add_right hx.2)
60+
end
61+
62+
lemma Ico_add_bij : bij_on (+d) (Ico a b) (Ico (a + d) (b + d)) :=
63+
begin
64+
rw [← Ici_inter_Iio, ← Ici_inter_Iio],
65+
exact (Ici_add_bij a d).inter_maps_to (λ x hx, add_lt_add_right hx _)
66+
(λ x hx, lt_of_add_lt_add_right hx.2)
67+
end
68+
69+
/-!
70+
### Images under `x ↦ x + a`
71+
-/
72+
73+
@[simp] lemma image_add_const_Ici : (λ x, x + a) '' Ici b = Ici (b + a) :=
74+
(Ici_add_bij _ _).image_eq
75+
76+
@[simp] lemma image_add_const_Ioi : (λ x, x + a) '' Ioi b = Ioi (b + a) :=
77+
(Ioi_add_bij _ _).image_eq
78+
79+
@[simp] lemma image_add_const_Icc : (λ x, x + a) '' Icc b c = Icc (b + a) (c + a) :=
80+
(Icc_add_bij _ _ _).image_eq
81+
82+
@[simp] lemma image_add_const_Ico : (λ x, x + a) '' Ico b c = Ico (b + a) (c + a) :=
83+
(Ico_add_bij _ _ _).image_eq
84+
85+
@[simp] lemma image_add_const_Ioc : (λ x, x + a) '' Ioc b c = Ioc (b + a) (c + a) :=
86+
(Ioc_add_bij _ _ _).image_eq
87+
88+
@[simp] lemma image_add_const_Ioo : (λ x, x + a) '' Ioo b c = Ioo (b + a) (c + a) :=
89+
(Ioo_add_bij _ _ _).image_eq
90+
91+
/-!
92+
### Images under `x ↦ a + x`
93+
-/
94+
95+
@[simp] lemma image_const_add_Ici : (λ x, a + x) '' Ici b = Ici (a + b) :=
96+
by simp only [add_comm a, image_add_const_Ici]
97+
98+
@[simp] lemma image_const_add_Ioi : (λ x, a + x) '' Ioi b = Ioi (a + b) :=
99+
by simp only [add_comm a, image_add_const_Ioi]
100+
101+
@[simp] lemma image_const_add_Icc : (λ x, a + x) '' Icc b c = Icc (a + b) (a + c) :=
102+
by simp only [add_comm a, image_add_const_Icc]
103+
104+
@[simp] lemma image_const_add_Ico : (λ x, a + x) '' Ico b c = Ico (a + b) (a + c) :=
105+
by simp only [add_comm a, image_add_const_Ico]
106+
107+
@[simp] lemma image_const_add_Ioc : (λ x, a + x) '' Ioc b c = Ioc (a + b) (a + c) :=
108+
by simp only [add_comm a, image_add_const_Ioc]
109+
110+
@[simp] lemma image_const_add_Ioo : (λ x, a + x) '' Ioo b c = Ioo (a + b) (a + c) :=
111+
by simp only [add_comm a, image_add_const_Ioo]
112+
113+
end set

0 commit comments

Comments
 (0)