chore(order/bounded_lattice): add is_compl.inf_left_eq_bot_iff etc (#3460)

Author: urkud

src/order/bounded_lattice.lean

@@ -1007,6 +1007,18 @@ lemma inf_sup {x' y'} (h : is_compl x y) (h' : is_compl x' y') :
   is_compl (x ⊓ x') (y ⊔ y') :=
 (h.symm.sup_inf h'.symm).symm
 
+lemma inf_left_eq_bot_iff (h : is_compl y z) : x ⊓ y = ⊥ ↔ x ≤ z :=
+inf_eq_bot_iff_le_compl h.sup_eq_top h.inf_eq_bot
+
+lemma inf_right_eq_bot_iff (h : is_compl y z) : x ⊓ z = ⊥ ↔ x ≤ y :=
+h.symm.inf_left_eq_bot_iff
+
+lemma disjoint_left_iff (h : is_compl y z) : disjoint x y ↔ x ≤ z :=
+disjoint_iff.trans h.inf_left_eq_bot_iff
+
+lemma disjoint_right_iff (h : is_compl y z) : disjoint x z ↔ x ≤ y :=
+h.symm.disjoint_left_iff
+
 end is_compl
 
 lemma is_compl_bot_top [bounded_lattice α] : is_compl (⊥ : α) ⊤ :=

src/topology/basic.lean

@@ -654,9 +654,7 @@ lemma closure_eq_cluster_pts {s : set α} : closure s = {a | cluster_pt a (𝓟
 calc closure s = (interior sᶜ)ᶜ : closure_eq_compl_interior_compl
   ... = {a | ¬ 𝓝 a ≤ 𝓟 sᶜ} : by rw [interior_eq_nhds]; refl
   ... = {a | cluster_pt a (𝓟 s)} : set.ext $ assume a, not_congr
-    (inf_eq_bot_iff_le_compl
-      (show 𝓟 s ⊔ 𝓟 sᶜ = ⊤, by simp only [sup_principal, union_compl_self, principal_univ])
-      (by simp only [inf_principal, inter_compl_self, principal_empty])).symm
+    (is_compl_principal s).inf_left_eq_bot_iff.symm
 
 theorem mem_closure_iff_cluster_pt {s : set α} {a : α} : a ∈ closure s ↔ cluster_pt a (𝓟 s) :=
 by simp only [closure_eq_cluster_pts, mem_set_of_eq]