[Merged by Bors] - feat(data/nat/pairing): add some nat.pair lemmas

src/data/nat/pairing.lean

@@ -132,3 +132,35 @@ lemma Union_unpair_prod {α β} {s : ℕ → set α} {t : ℕ → set β} :
 by { rw [← Union_prod], convert surjective_unpair.Union_comp _, refl }
 
 end set
+
+section complete_lattice
+
+lemma supr_unpair_sup {α} [complete_lattice α] {s t : ℕ → α} :
+  (⨆ n : ℕ, s n.unpair.1 ⊔ t n.unpair.2) = (⨆ i : ℕ, s i) ⊔ ⨆ j, t j :=
+begin
+  simp_rw [supr_sup, sup_supr, ← (supr_prod : (⨆ i : ℕ × ℕ, s i.1 ⊔ t i.2) = _),
+           ← nat.surjective_unpair.supr_comp],
+end
+
+lemma supr_unpair_inf {α} [complete_distrib_lattice α] {s t : ℕ → α} :
+  (⨆ n : ℕ, s n.unpair.1 ⊓ t n.unpair.2) = (⨆ i : ℕ, s i) ⊓ ⨆ j, t j :=
+begin
+  simp_rw [supr_inf_eq, inf_supr_eq, ← (supr_prod : (⨆ i : ℕ × ℕ, s i.1 ⊓ t i.2) = _),
+           ← nat.surjective_unpair.supr_comp],
+end
+
+lemma infi_unpair_sup {α} [complete_distrib_lattice α] {s t : ℕ → α} :
+  (⨅ n : ℕ, s n.unpair.1 ⊔ t n.unpair.2) = (⨅ i : ℕ, s i) ⊔ ⨅ j, t j :=
+begin
+  simp_rw [infi_sup_eq, sup_infi_eq, ← (infi_prod : (⨅ i : ℕ × ℕ, s i.1 ⊔ t i.2) = _),
+           ← nat.surjective_unpair.infi_comp],
+end
+
+lemma infi_unpair_inf {α} [complete_lattice α] {s t : ℕ → α} :
+  (⨅ n : ℕ, s n.unpair.1 ⊓ t n.unpair.2) = (⨅ i : ℕ, s i) ⊓ ⨅ j, t j :=
+begin
+  simp_rw [infi_inf, inf_infi, ← (infi_prod : (⨅ i : ℕ × ℕ, s i.1 ⊓ t i.2) = _),
+           ← nat.surjective_unpair.infi_comp],
+end
+
+end complete_lattice