feat(order/interval): Order intervals (#14807)

Define `nonempty_interval`, the type of nonempty intervals in an order, namely pairs where the second element is greater than the first, and `interval α` as `with_bot (nonempty_interval α)`.

src/data/option/basic.lean

@@ -32,7 +32,7 @@ along with a term `a : α` if the value is `true`.
 -/
 
 namespace option
-variables {α : Type*} {β : Type*} {γ : Type*}
+variables {α β γ δ : Type*}
 
 lemma coe_def : (coe : α → option α) = some := rfl
 
@@ -189,6 +189,10 @@ by { cases x; simp only [map_none', map_some', h, mem_def] }
   option.map h (option.map g x) = option.map (h ∘ g) x :=
 by { cases x; simp only [map_none', map_some'] }
 
+lemma map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
+  (option.map f₁ a).map g₁ = (option.map f₂ a).map g₂ :=
+by rw [map_map, h, ←map_map]
+
 lemma comp_map (h : β → γ) (g : α → β) (x : option α) :
   option.map (h ∘ g) x = option.map h (option.map g x) := (map_map _ _ _).symm
 

src/data/set/lattice.lean

@@ -294,6 +294,18 @@ explicit for this purpose. -/
 lemma Inter_subset_of_subset {s : ι → set α} {t : set α} (i : ι) (h : s i ⊆ t) : (⋂ i, s i) ⊆ t :=
 @infi_le_of_le (set α) _ _ _ _ i h
 
+/-- This rather trivial consequence of `subset_Union₂` is convenient with `apply`, and has `i` and
+`j` explicit for this purpose. -/
+lemma subset_Union₂_of_subset {s : set α} {t : Π i, κ i → set α} (i : ι) (j : κ i) (h : s ⊆ t i j) :
+  s ⊆ ⋃ i j, t i j :=
+@le_supr₂_of_le (set α) _ _ _ _ _ i j h
+
+/-- This rather trivial consequence of `Inter₂_subset` is convenient with `apply`, and has `i` and
+`j` explicit for this purpose. -/
+lemma Inter₂_subset_of_subset {s : Π i, κ i → set α} {t : set α} (i : ι) (j : κ i) (h : s i j ⊆ t) :
+  (⋂ i j, s i j) ⊆ t :=
+@infi₂_le_of_le (set α) _ _ _ _ _ i j h
+
 lemma Union_mono {s t : ι → set α} (h : ∀ i, s i ⊆ t i) : (⋃ i, s i) ⊆ ⋃ i, t i :=
 @supr_mono (set α) _ _ s t h
 

src/order/bounded_order.lean

@@ -35,13 +35,13 @@ instances for `Prop` and `fun`.
   Typical examples include `Prop` and `set α`.
 -/
 
-open order_dual
+open function order_dual
 
 set_option old_structure_cmd true
 
 universes u v
 
-variables {α : Type u} {β : Type v}
+variables {α : Type u} {β : Type v} {γ δ : Type*}
 
 /-! ### Top, bottom element -/
 
@@ -548,6 +548,9 @@ meta instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (with_
 
 instance : inhabited (with_bot α) := ⟨⊥⟩
 
+lemma coe_injective : injective (coe : α → with_bot α) := option.some_injective _
+@[norm_cast] lemma coe_inj : (a : with_bot α) = b ↔ a = b := option.some_inj
+
 lemma none_eq_bot : (none : with_bot α) = (⊥ : with_bot α) := rfl
 lemma some_eq_coe (a : α) : (some a : with_bot α) = (↑a : with_bot α) := rfl
 
@@ -580,6 +583,10 @@ def map (f : α → β) : with_bot α → with_bot β := option.map f
 @[simp] lemma map_bot (f : α → β) : map f ⊥ = ⊥ := rfl
 @[simp] lemma map_coe (f : α → β) (a : α) : map f a = f a := rfl
 
+lemma map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
+  map g₁ (map f₁ a) = map g₂ (map f₂ a) :=
+option.map_comm h _
+
 lemma ne_bot_iff_exists {x : with_bot α} : x ≠ ⊥ ↔ ∃ (a : α), ↑a = x := option.ne_none_iff_exists
 
 /-- Deconstruct a `x : with_bot α` to the underlying value in `α`, given a proof that `x ≠ ⊥`. -/
@@ -917,6 +924,10 @@ def map (f : α → β) : with_top α → with_top β := option.map f
 @[simp] lemma map_top (f : α → β) : map f ⊤ = ⊤ := rfl
 @[simp] lemma map_coe (f : α → β) (a : α) : map f a = f a := rfl
 
+lemma map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
+  map g₁ (map f₁ a) = map g₂ (map f₂ a) :=
+option.map_comm h _
+
 lemma map_to_dual (f : αᵒᵈ → βᵒᵈ) (a : with_bot α) :
   map f (with_bot.to_dual a) = a.map (to_dual ∘ f) := rfl
 lemma map_of_dual (f : α → β) (a : with_bot αᵒᵈ) :