chore(data/finset/locally_finite): add more lemmas about one-sided in…

…tervals (#17033)

This also:
 * adds new `pi.locally_finite_order_bot` and `pi.locally_finite_order_top` instances, and generalizes the lemmas needed to prove things about them.
* generalizes some `finsupp` lemmas about intervals to arbitrary `decidable` arguments.

src/analysis/inner_product_space/gram_schmidt_ortho.lean

@@ -238,7 +238,7 @@ begin
   have : ↑(((b.repr) (gram_schmidt 𝕜 b i)).support) ⊆ set.Iio j,
     from basis.repr_support_subset_of_mem_span b (set.Iio j) this,
   exact (finsupp.mem_supported' _ _).1
-    ((finsupp.mem_supported 𝕜 _).2 this) j (not_mem_Iio.2 (le_refl j)),
+    ((finsupp.mem_supported 𝕜 _).2 this) j set.not_mem_Iio_self,
 end
 
 /-- `gram_schmidt` produces linearly independent vectors when given linearly independent vectors. -/

src/data/dfinsupp/interval.lean

@@ -167,4 +167,20 @@ lemma card_Ioo : (Ioo f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (
 by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
 
 end locally_finite
+
+section canonically_ordered
+variables [decidable_eq ι] [Π i, decidable_eq (α i)]
+variables [Π i, canonically_ordered_add_monoid (α i)] [Π i, locally_finite_order (α i)]
+
+variables (f : Π₀ i, α i)
+
+lemma card_Iic : (Iic f).card = ∏ i in f.support, (Iic (f i)).card :=
+by simp_rw [Iic_eq_Icc, card_Icc, dfinsupp.bot_eq_zero, support_zero, empty_union, zero_apply,
+  bot_eq_zero]
+
+lemma card_Iio : (Iio f).card = ∏ i in f.support, (Iic (f i)).card - 1 :=
+by rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
+
+end canonically_ordered
+
 end dfinsupp

src/data/finset/interval.lean

@@ -87,4 +87,12 @@ by rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]
 lemma card_Ioo_finset (h : s ⊆ t) : (Ioo s t).card = 2 ^ (t.card - s.card) - 2 :=
 by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]
 
+/-- Cardinality of an `Iic` of finsets. -/
+lemma card_Iic_finset : (Iic s).card = 2 ^ s.card :=
+by rw [Iic_eq_powerset, card_powerset]
+
+/-- Cardinality of an `Iio` of finsets. -/
+lemma card_Iio_finset : (Iio s).card = 2 ^ s.card - 1 :=
+by rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]
+
 end finset

src/data/finset/locally_finite.lean

@@ -374,37 +374,54 @@ lemma card_Ioo_eq_card_Ioc_sub_one (a b : α) : (Ioo a b).card = (Ioc a b).card
 lemma card_Ioo_eq_card_Icc_sub_two (a b : α) : (Ioo a b).card = (Icc a b).card - 2 :=
 by { rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one], refl }
 
+end partial_order
+
+section bounded_partial_order
+variables [partial_order α]
+
 section order_top
-variables [order_top α]
+variables [locally_finite_order_top α]
 
-@[simp] lemma Ici_erase [decidable_eq α] (a : α) : (Ici a).erase a = Ioi a := Icc_erase_left _ _
+@[simp] lemma Ici_erase [decidable_eq α] (a : α) : (Ici a).erase a = Ioi a :=
+by { ext, simp_rw [finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm], }
 @[simp] lemma Ioi_insert [decidable_eq α] (a : α) : insert a (Ioi a) = Ici a :=
-Ioc_insert_left le_top
+by { ext, simp_rw [finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm] }
+
+@[simp] lemma not_mem_Ioi_self {b : α} : b ∉ Ioi b := λ h, lt_irrefl _ (mem_Ioi.1 h)
 
 -- Purposefully written the other way around
-lemma Ici_eq_cons_Ioi (a : α) : Ici a = (Ioi a).cons a left_not_mem_Ioc :=
+lemma Ici_eq_cons_Ioi (a : α) : Ici a = (Ioi a).cons a not_mem_Ioi_self :=
 by { classical, rw [cons_eq_insert, Ioi_insert] }
 
+lemma card_Ioi_eq_card_Ici_sub_one (a : α) : (Ioi a).card = (Ici a).card - 1 :=
+by rw [Ici_eq_cons_Ioi, card_cons, add_tsub_cancel_right]
+
 end order_top
 
 section order_bot
-variables [order_bot α]
+variables [locally_finite_order_bot α]
 
-@[simp] lemma Iic_erase [decidable_eq α] (b : α) : (Iic b).erase b = Iio b := Icc_erase_right _ _
+@[simp] lemma Iic_erase [decidable_eq α] (b : α) : (Iic b).erase b = Iio b :=
+by { ext, simp_rw [finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm] }
 @[simp] lemma Iio_insert [decidable_eq α] (b : α) : insert b (Iio b) = Iic b :=
-Ico_insert_right bot_le
+by { ext, simp_rw [finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm] }
+
+@[simp] lemma not_mem_Iio_self {b : α} : b ∉ Iio b := λ h, lt_irrefl _ (mem_Iio.1 h)
 
 -- Purposefully written the other way around
-lemma Iic_eq_cons_Iio (b : α) : Iic b = (Iio b).cons b right_not_mem_Ico :=
+lemma Iic_eq_cons_Iio (b : α) : Iic b = (Iio b).cons b not_mem_Iio_self :=
 by { classical, rw [cons_eq_insert, Iio_insert] }
 
+lemma card_Iio_eq_card_Iic_sub_one (a : α) : (Iio a).card = (Iic a).card - 1 :=
+by rw [Iic_eq_cons_Iio, card_cons, add_tsub_cancel_right]
+
 end order_bot
-end partial_order
+
+end bounded_partial_order
 
 section linear_order
 variables [linear_order α]
 
-
 section locally_finite_order
 variables [locally_finite_order α] {a b : α}
 

src/data/finsupp/interval.lean

@@ -51,7 +51,7 @@ section range_Icc
 variables [has_zero α] [partial_order α] [locally_finite_order α] {f g : ι →₀ α} {i : ι} {a : α}
 
 /-- Pointwise `finset.Icc` bundled as a `finsupp`. -/
-@[simps] def range_Icc (f g : ι →₀ α) : ι →₀ finset α :=
+@[simps to_fun] def range_Icc (f g : ι →₀ α) : ι →₀ finset α :=
 { to_fun := λ i, Icc (f i) (g i),
   support := f.support ∪ g.support,
   mem_support_to_fun := λ i, begin
@@ -60,33 +60,60 @@ variables [has_zero α] [partial_order α] [locally_finite_order α] {f g : ι 
     exact Icc_eq_singleton_iff.symm,
   end }
 
+@[simp] lemma range_Icc_support [decidable_eq ι] (f g : ι →₀ α) :
+  (range_Icc f g).support = f.support ∪ g.support :=
+by convert rfl
+
 lemma mem_range_Icc_apply_iff : a ∈ f.range_Icc g i ↔ f i ≤ a ∧ a ≤ g i := mem_Icc
 
 end range_Icc
 
+section partial_order
 variables [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α)
 
 instance : locally_finite_order (ι →₀ α) :=
 locally_finite_order.of_Icc (ι →₀ α)
   (λ f g, (f.support ∪ g.support).finsupp $ f.range_Icc g)
   (λ f g x, begin
-    refine (mem_finsupp_iff_of_support_subset $ subset.rfl).trans _,
+    refine (mem_finsupp_iff_of_support_subset $ finset.subset_of_eq $
+      range_Icc_support _ _).trans _,
     simp_rw mem_range_Icc_apply_iff,
     exact forall_and_distrib,
   end)
 
-lemma Icc_eq : Icc f g = (f.support ∪ g.support).finsupp (f.range_Icc g) := rfl
+lemma Icc_eq [decidable_eq ι] : Icc f g = (f.support ∪ g.support).finsupp (f.range_Icc g) :=
+by convert rfl
 
-lemma card_Icc : (Icc f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card :=
-card_finsupp _ _
+lemma card_Icc [decidable_eq ι] :
+  (Icc f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card :=
+by simp_rw [Icc_eq, card_finsupp, range_Icc_to_fun]
 
-lemma card_Ico : (Ico f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 1 :=
+lemma card_Ico [decidable_eq ι] :
+  (Ico f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 1 :=
 by rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
 
-lemma card_Ioc : (Ioc f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 1 :=
+lemma card_Ioc [decidable_eq ι] :
+  (Ioc f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 1 :=
 by rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
 
-lemma card_Ioo : (Ioo f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 2 :=
+lemma card_Ioo [decidable_eq ι] :
+  (Ioo f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 2 :=
 by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
 
+end partial_order
+
+section canonically_ordered
+variables [canonically_ordered_add_monoid α] [locally_finite_order α]
+
+variables (f : ι →₀ α)
+
+lemma card_Iic : (Iic f).card = ∏ i in f.support, (Iic (f i)).card :=
+by simp_rw [Iic_eq_Icc, card_Icc, finsupp.bot_eq_zero, support_zero, empty_union, zero_apply,
+  bot_eq_zero]
+
+lemma card_Iio : (Iio f).card = ∏ i in f.support, (Iic (f i)).card - 1 :=
+by rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
+
+end canonically_ordered
+
 end finsupp

src/data/pi/interval.lean

@@ -16,15 +16,19 @@ order are locally finite and calculates the cardinality of their intervals.
 open finset fintype
 open_locale big_operators
 
-variables {ι : Type*} {α : ι → Type*} [decidable_eq ι] [fintype ι] [Π i, decidable_eq (α i)]
-  [Π i, partial_order (α i)] [Π i, locally_finite_order (α i)]
+variables {ι : Type*} {α : ι → Type*}
+
 
 namespace pi
 
+section locally_finite
+variables [decidable_eq ι] [fintype ι] [Π i, decidable_eq (α i)]
+  [Π i, partial_order (α i)] [Π i, locally_finite_order (α i)]
+
 instance : locally_finite_order (Π i, α i) :=
 locally_finite_order.of_Icc _
   (λ a b, pi_finset $ λ i, Icc (a i) (b i))
-  (λ a b x, by { simp_rw [mem_pi_finset, mem_Icc], exact forall_and_distrib })
+  (λ a b x, by simp_rw [mem_pi_finset, mem_Icc, le_def, forall_and_distrib])
 
 variables (a b : Π i, α i)
 
@@ -41,4 +45,41 @@ by rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
 lemma card_Ioo : (Ioo a b).card = (∏ i, (Icc (a i) (b i)).card) - 2 :=
 by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
 
+end locally_finite
+
+section bounded
+variables [decidable_eq ι] [fintype ι] [Π i, decidable_eq (α i)] [Π i, partial_order (α i)]
+
+section bot
+variables [Π i, locally_finite_order_bot (α i)] (b : Π i, α i)
+
+instance : locally_finite_order_bot (Π i, α i) :=
+locally_finite_order_top.of_Iic _
+  (λ b, pi_finset $ λ i, Iic (b i))
+  (λ b x, by simp_rw [mem_pi_finset, mem_Iic, le_def])
+
+lemma card_Iic : (Iic b).card = ∏ i, (Iic (b i)).card := card_pi_finset _
+
+lemma card_Iio : (Iio b).card = (∏ i, (Iic (b i)).card) - 1 :=
+by rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
+
+end bot
+
+section top
+variables [Π i, locally_finite_order_top (α i)] (a : Π i, α i)
+
+instance : locally_finite_order_top (Π i, α i) :=
+locally_finite_order_top.of_Ici _
+  (λ a, pi_finset $ λ i, Ici (a i))
+  (λ a x, by simp_rw [mem_pi_finset, mem_Ici, le_def])
+
+lemma card_Ici : (Ici a).card = (∏ i, (Ici (a i)).card) := card_pi_finset _
+
+lemma card_Ioi : (Ioi a).card = (∏ i, (Ici (a i)).card) - 1 :=
+by rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]
+
+end top
+
+end bounded
+
 end pi

src/data/set/intervals/basic.lean

@@ -607,6 +607,10 @@ lemma not_mem_Ioi : c ∉ Ioi a ↔ c ≤ a := not_lt
 
 lemma not_mem_Iio : c ∉ Iio b ↔ b ≤ c := not_lt
 
+@[simp] lemma not_mem_Ioi_self : a ∉ Ioi a := lt_irrefl _
+
+@[simp] lemma not_mem_Iio_self : b ∉ Iio b := lt_irrefl _
+
 lemma not_mem_Ioc_of_le (ha : c ≤ a) : c ∉ Ioc a b :=
 not_mem_subset Ioc_subset_Ioi_self $ not_mem_Ioi.mpr ha