feat(order/bounded_lattice): add is_compl.le_sup_right_iff_inf_left_le (#10014)

This lemma is a generalization of `is_compl.inf_left_eq_bot_iff`.
Also drop `inf_eq_bot_iff_le_compl` in favor of
`is_compl.inf_left_eq_bot_iff` and add
`set.subset_union_compl_iff_inter_subset`.

Author: urkud

src/data/set/basic.lean

@@ -891,6 +891,9 @@ theorem compl_subset_comm {s t : set α} : sᶜ ⊆ t ↔ tᶜ ⊆ s := @compl_l
 
 @[simp] lemma compl_subset_compl {s t : set α} : sᶜ ⊆ tᶜ ↔ t ⊆ s := @compl_le_compl_iff_le _ t s _
 
+theorem subset_union_compl_iff_inter_subset {s t u : set α} : s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t :=
+(@is_compl_compl _ u _).le_sup_right_iff_inf_left_le
+
 theorem compl_subset_iff_union {s t : set α} : sᶜ ⊆ t ↔ s ∪ t = univ :=
 iff.symm $ eq_univ_iff_forall.trans $ forall_congr $ λ a, or_iff_not_imp_left
 

src/order/bounded_lattice.lean

@@ -312,17 +312,6 @@ class distrib_lattice_bot α extends distrib_lattice α, semilattice_inf_bot α,
 /-- A bounded distributive lattice is exactly what it sounds like. -/
 class bounded_distrib_lattice α extends distrib_lattice_bot α, bounded_lattice α
 
-lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α}
-  (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c :=
-⟨λ h,
-  calc a ≤ a ⊓ (b ⊔ c) : by simp [h₁]
-    ... = (a ⊓ b) ⊔ (a ⊓ c) : by simp [inf_sup_left]
-    ... ≤ c : by simp [h, inf_le_right],
-  λ h,
-  bot_unique $
-    calc a ⊓ b ≤ b ⊓ c : by { rw inf_comm, exact inf_le_inf_left _ h }
-      ... = ⊥ : h₂⟩
-
 /-- Propositions form a bounded distributive lattice. -/
 instance Prop.bounded_distrib_lattice : bounded_distrib_lattice Prop :=
 { le           := λ a b, a → b,
@@ -1169,10 +1158,19 @@ lemma to_order_dual (h : is_compl x y) : is_compl (to_dual x) (to_dual y) := ⟨
 
 end bounded_lattice
 
-variables [bounded_distrib_lattice α] {x y z : α}
+variables [bounded_distrib_lattice α] {a b x y z : α}
+
+lemma inf_left_le_of_le_sup_right (h : is_compl x y) (hle : a ≤ b ⊔ y) : a ⊓ x ≤ b :=
+calc a ⊓ x ≤ (b ⊔ y) ⊓ x : inf_le_inf hle le_rfl
+... = (b ⊓ x) ⊔ (y ⊓ x) : inf_sup_right
+... = b ⊓ x : by rw [h.symm.inf_eq_bot, sup_bot_eq]
+... ≤ b : inf_le_left
+
+lemma le_sup_right_iff_inf_left_le {a b} (h : is_compl x y) : a ≤ b ⊔ y ↔ a ⊓ x ≤ b :=
+⟨h.inf_left_le_of_le_sup_right, h.symm.to_order_dual.inf_left_le_of_le_sup_right⟩
 
 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
+by rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
 
 lemma inf_right_eq_bot_iff (h : is_compl y z) : x ⊓ z = ⊥ ↔ x ≤ y :=
 h.symm.inf_left_eq_bot_iff

src/topology/uniform_space/separation.lean

@@ -203,8 +203,7 @@ instance separated_regular [separated_space α] : regular_space α :=
         h this rfl,
     have closure e ∈ 𝓝 a, from (𝓝 a).sets_of_superset (mem_nhds_left a hd) subset_closure,
     have 𝓝 a ⊓ 𝓟 (closure e)ᶜ = ⊥,
-      from (@inf_eq_bot_iff_le_compl _ _ _ (𝓟 (closure e)ᶜ) (𝓟 (closure e))
-        (by simp [principal_univ, union_comm]) (by simp)).mpr (by simp [this]),
+      from (is_compl_principal (closure e)).inf_right_eq_bot_iff.2 (le_principal_iff.2 this),
     ⟨(closure e)ᶜ, is_closed_closure.is_open_compl, assume x h₁ h₂, @e_subset x h₂ h₁, this⟩,
     ..@t2_space.t1_space _ _ (separated_iff_t2.mp ‹_›) }