[Merged by Bors] - feat(data/sigma/interval): A disjoint sum of locally finite orders is locally finite

src/data/sigma/interval.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.sigma.order
+import order.locally_finite
+
+/-!
+# Finite intervals in a sigma type
+
+This file provides the `locally_finite_order` instance for the disjoint sum of orders `Σ i, α i` and
+calculates the cardinality of its finite intervals.
+
+## TODO
+
+Do the same for the lexicographical order
+-/
+
+open finset function
+
+namespace sigma
+variables {ι : Type*} {α : ι → Type*}
+
+/-! ### Disjoint sum of orders -/
+
+section disjoint
+variables [decidable_eq ι] [Π i, preorder (α i)] [Π i, locally_finite_order (α i)]
+
+instance : locally_finite_order (Σ i, α i) :=
+{ finset_Icc := sigma_lift (λ _, Icc),
+  finset_Ico := sigma_lift (λ _, Ico),
+  finset_Ioc := sigma_lift (λ _, Ioc),
+  finset_Ioo := sigma_lift (λ _, Ioo),
+  finset_mem_Icc := λ ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩, begin
+    simp_rw [mem_sigma_lift, le_def, mem_Icc, exists_and_distrib_left, ←exists_and_distrib_right,
+      ←exists_prop],
+    exact bex_congr (λ _ _, by split; rintro ⟨⟨⟩, ht⟩; exact ⟨rfl, ht⟩),
+  end,
+  finset_mem_Ico := λ ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩, begin
+    simp_rw [mem_sigma_lift, le_def, lt_def, mem_Ico, exists_and_distrib_left,
+      ←exists_and_distrib_right, ←exists_prop],
+    exact bex_congr (λ _ _, by split; rintro ⟨⟨⟩, ht⟩; exact ⟨rfl, ht⟩),
+  end,
+  finset_mem_Ioc := λ ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩, begin
+    simp_rw [mem_sigma_lift, le_def, lt_def, mem_Ioc, exists_and_distrib_left,
+      ←exists_and_distrib_right, ←exists_prop],
+    exact bex_congr (λ _ _, by split; rintro ⟨⟨⟩, ht⟩; exact ⟨rfl, ht⟩),
+  end,
+  finset_mem_Ioo := λ ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩, begin
+    simp_rw [mem_sigma_lift, lt_def, mem_Ioo, exists_and_distrib_left, ←exists_and_distrib_right,
+      ←exists_prop],
+    exact bex_congr (λ _ _, by split; rintro ⟨⟨⟩, ht⟩; exact ⟨rfl, ht⟩),
+  end }
+
+section
+variables (a b : Σ i, α i)
+
+lemma card_Icc : (Icc a b).card = if h : a.1 = b.1 then (Icc (h.rec a.2) b.2).card else 0 :=
+card_sigma_lift _ _ _
+
+lemma card_Ico : (Ico a b).card = if h : a.1 = b.1 then (Ico (h.rec a.2) b.2).card else 0 :=
+card_sigma_lift _ _ _
+
+lemma card_Ioc : (Ioc a b).card = if h : a.1 = b.1 then (Ioc (h.rec a.2) b.2).card else 0 :=
+card_sigma_lift _ _ _
+
+lemma card_Ioo : (Ioo a b).card = if h : a.1 = b.1 then (Ioo (h.rec a.2) b.2).card else 0 :=
+card_sigma_lift _ _ _
+
+end
+
+variables (i : ι) (a b : α i)
+
+@[simp] lemma Icc_mk_mk : Icc (⟨i, a⟩ : sigma α) ⟨i, b⟩ = (Icc a b).map (embedding.sigma_mk i) :=
+dif_pos rfl
+
+@[simp] lemma Ico_mk_mk : Ico (⟨i, a⟩ : sigma α) ⟨i, b⟩ = (Ico a b).map (embedding.sigma_mk i) :=
+dif_pos rfl
+
+@[simp] lemma Ioc_mk_mk : Ioc (⟨i, a⟩ : sigma α) ⟨i, b⟩ = (Ioc a b).map (embedding.sigma_mk i) :=
+dif_pos rfl
+
+@[simp] lemma Ioo_mk_mk : Ioo (⟨i, a⟩ : sigma α) ⟨i, b⟩ = (Ioo a b).map (embedding.sigma_mk i) :=
+dif_pos rfl
+
+end disjoint
+end sigma

src/data/sigma/order.lean

@@ -30,15 +30,59 @@ variables {ι : Type*} {α : ι → Type*}
 inductive le [Π i, has_le (α i)] : Π a b : Σ i, α i, Prop
 | fiber (i : ι) (a b : α i) : a ≤ b → le ⟨i, a⟩ ⟨i, b⟩
 
+/-- Disjoint sum of orders. `⟨i, a⟩ < ⟨j, b⟩` iff `i = j` and `a < b`. -/
+inductive lt [Π i, has_lt (α i)] : Π a b : Σ i, α i, Prop
+| fiber (i : ι) (a b : α i) : a < b → lt ⟨i, a⟩ ⟨i, b⟩
+
 instance [Π i, has_le (α i)] : has_le (Σ i, α i) := ⟨le⟩
+instance [Π i, has_lt (α i)] : has_lt (Σ i, α i) := ⟨lt⟩
+
+@[simp] lemma mk_le_mk_iff [Π i, has_le (α i)] {i : ι} {a b : α i} :
+  (⟨i, a⟩ : sigma α) ≤ ⟨i, b⟩ ↔ a ≤ b :=
+⟨λ ⟨_, _, _, h⟩, h, le.fiber _ _ _⟩
+
+@[simp] lemma mk_lt_mk_iff [Π i, has_lt (α i)] {i : ι} {a b : α i} :
+  (⟨i, a⟩ : sigma α) < ⟨i, b⟩ ↔ a < b :=
+⟨λ ⟨_, _, _, h⟩, h, lt.fiber _ _ _⟩
+
+lemma le_def [Π i, has_le (α i)] {a b : Σ i, α i} : a ≤ b ↔ ∃ h : a.1 = b.1, h.rec a.2 ≤ b.2 :=
+begin
+  split,
+  { rintro ⟨i, a, b, h⟩,
+    exact ⟨rfl, h⟩ },
+  { obtain ⟨i, a⟩ := a,
+    obtain ⟨j, b⟩ := b,
+    rintro ⟨(rfl : i = j), h⟩,
+    exact le.fiber _ _ _ h }
+end
+
+lemma lt_def [Π i, has_lt (α i)] {a b : Σ i, α i} : a < b ↔ ∃ h : a.1 = b.1, h.rec a.2 < b.2 :=
+begin
+  split,
+  { rintro ⟨i, a, b, h⟩,
+    exact ⟨rfl, h⟩ },
+  { obtain ⟨i, a⟩ := a,
+    obtain ⟨j, b⟩ := b,
+    rintro ⟨(rfl : i = j), h⟩,
+    exact lt.fiber _ _ _ h }
+end
 
 instance [Π i, preorder (α i)] : preorder (Σ i, α i) :=
 { le_refl := λ ⟨i, a⟩, le.fiber i a a le_rfl,
   le_trans := begin
     rintro _ _ _ ⟨i, a, b, hab⟩ ⟨_, _, c, hbc⟩,
     exact le.fiber i a c (hab.trans hbc),
   end,
-  .. sigma.has_le }
+  lt_iff_le_not_le := λ _ _, begin
+    split,
+    { rintro ⟨i, a, b, hab⟩,
+      rwa [mk_le_mk_iff, mk_le_mk_iff, ←lt_iff_le_not_le] },
+    { rintro ⟨⟨i, a, b, hab⟩, h⟩,
+      rw mk_le_mk_iff at h,
+      exact mk_lt_mk_iff.2 (hab.lt_of_not_le h) }
+  end,
+  .. sigma.has_le,
+  .. sigma.has_lt }
 
 instance [Π i, partial_order (α i)] : partial_order (Σ i, α i) :=
 { le_antisymm := begin

src/order/locally_finite.lean

@@ -60,6 +60,7 @@ Instances for concrete types are proved in their respective files:
 * `ℕ+` is in `data.pnat.interval`
 * `fin n` is in `data.fin.interval`
 * `finset α` is in `data.finset.interval`
+* `Σ i, α i` is in `data.sigma.interval`
 Along, you will find lemmas about the cardinality of those finite intervals.
 
 ## TODO