feat(order/lattice): add left_lt_inf etc (#14152)

* add `left_lt_sup`, `right_lt_sup`, `left_or_right_lt_sup`, and their `inf` counterparts;
* generalize `is_top_or_exists_gt` and `is_bot_or_exists_lt` to directed orders, replacing `forall_le_or_exists_lt_inf` and `forall_le_or_exists_lt_sup`;
* generalize `exists_lt_of_sup` and `exists_lt_of_inf` to directed orders, rename them to `exists_lt_of_directed_le` and `exists_lt_of_directed_ge`.

Author: urkud

src/order/directed.lean

@@ -137,11 +137,29 @@ protected lemma is_min.is_bot [is_directed α (swap (≤))] (h : is_min a) : is_
 protected lemma is_max.is_top [is_directed α (≤)] (h : is_max a) : is_top a :=
 λ b, let ⟨c, hac, hbc⟩ := exists_ge_ge a b in hbc.trans $ h hac
 
+lemma is_top_or_exists_gt [is_directed α (≤)] (a : α) : is_top a ∨ (∃ b, a < b) :=
+(em (is_max a)).imp is_max.is_top not_is_max_iff.mp
+
+lemma is_bot_or_exists_lt [is_directed α (swap (≤))] (a : α) : is_bot a ∨ (∃ b, b < a) :=
+@is_top_or_exists_gt αᵒᵈ _ _ a
+
 lemma is_bot_iff_is_min [is_directed α (swap (≤))] : is_bot a ↔ is_min a :=
 ⟨is_bot.is_min, is_min.is_bot⟩
 
 lemma is_top_iff_is_max [is_directed α (≤)] : is_top a ↔ is_max a := ⟨is_top.is_max, is_max.is_top⟩
 
+variables (β) [partial_order β]
+
+theorem exists_lt_of_directed_ge [is_directed β (swap (≤))] [nontrivial β] : ∃ a b : β, a < b :=
+begin
+  rcases exists_pair_ne β with ⟨a, b, hne⟩,
+  rcases is_bot_or_exists_lt a with ha|⟨c, hc⟩,
+  exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]
+end
+
+theorem exists_lt_of_directed_le [is_directed β (≤)] [nontrivial β] : ∃ a b : β, a < b :=
+let ⟨a, b, h⟩ := exists_lt_of_directed_ge βᵒᵈ in ⟨b, a, h⟩
+
 end preorder
 
 @[priority 100]  -- see Note [lower instance priority]

src/order/lattice.lean

@@ -165,6 +165,9 @@ sup_eq_left.2 h
 @[simp] theorem left_eq_sup : a = a ⊔ b ↔ b ≤ a :=
 eq_comm.trans sup_eq_left
 
+@[simp] theorem left_lt_sup : a < a ⊔ b ↔ ¬b ≤ a :=
+le_sup_left.lt_iff_ne.trans $ not_congr left_eq_sup
+
 @[simp] theorem sup_eq_right : a ⊔ b = b ↔ a ≤ b :=
 le_antisymm_iff.trans $ by simp [le_refl]
 
@@ -174,6 +177,12 @@ sup_eq_right.2 h
 @[simp] theorem right_eq_sup : b = a ⊔ b ↔ a ≤ b :=
 eq_comm.trans sup_eq_right
 
+@[simp] theorem right_lt_sup : b < a ⊔ b ↔ ¬a ≤ b :=
+le_sup_right.lt_iff_ne.trans $ not_congr right_eq_sup
+
+lemma left_or_right_lt_sup (h : a ≠ b) : (a < a ⊔ b ∨ b < a ⊔ b) :=
+h.not_le_or_not_le.symm.imp left_lt_sup.2 right_lt_sup.2
+
 theorem sup_le_sup (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d :=
 sup_le (le_sup_of_le_left h₁) (le_sup_of_le_right h₂)
 
@@ -225,12 +234,6 @@ by rw [sup_sup_sup_comm, sup_idem]
 lemma sup_sup_distrib_right (a b c : α) : (a ⊔ b) ⊔ c = (a ⊔ c) ⊔ (b ⊔ c) :=
 by rw [sup_sup_sup_comm, sup_idem]
 
-lemma forall_le_or_exists_lt_sup (a : α) : (∀b, b ≤ a) ∨ (∃b, a < b) :=
-suffices (∃b, ¬b ≤ a) → (∃b, a < b),
-  by rwa [or_iff_not_imp_left, not_forall],
-assume ⟨b, hb⟩,
-⟨a ⊔ b, lt_of_le_of_ne le_sup_left $ mt left_eq_sup.1 hb⟩
-
 /-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`. -/
 theorem monotone.forall_le_of_antitone {β : Type*} [preorder β] {f g : α → β}
   (hf : monotone f) (hg : antitone g) (h : f ≤ g) (m n : α) :
@@ -254,13 +257,6 @@ begin
   injection this; congr'
 end
 
-theorem exists_lt_of_sup (α : Type*) [semilattice_sup α] [nontrivial α] : ∃ a b : α, a < b :=
-begin
-  rcases exists_pair_ne α with ⟨a, b, hne⟩,
-  rcases forall_le_or_exists_lt_sup b with (hb|H),
-  exacts [⟨a, b, (hb a).lt_of_ne hne⟩, ⟨b, H⟩]
-end
-
 lemma ite_le_sup (s s' : α) (P : Prop) [decidable P] : ite P s s' ≤ s ⊔ s' :=
 if h : P then (if_pos h).trans_le le_sup_left else (if_neg h).trans_le le_sup_right
 
@@ -329,6 +325,8 @@ lt_of_le_of_lt inf_le_right h
 @[simp] theorem inf_eq_left : a ⊓ b = a ↔ a ≤ b :=
 le_antisymm_iff.trans $ by simp [le_refl]
 
+@[simp] theorem inf_lt_left : a ⊓ b < a ↔ ¬a ≤ b := @left_lt_sup αᵒᵈ _ _ _
+
 theorem inf_of_le_left (h : a ≤ b) : a ⊓ b = a :=
 inf_eq_left.2 h
 
@@ -338,6 +336,11 @@ eq_comm.trans inf_eq_left
 @[simp] theorem inf_eq_right : a ⊓ b = b ↔ b ≤ a :=
 le_antisymm_iff.trans $ by simp [le_refl]
 
+@[simp] theorem inf_lt_right : a ⊓ b < b ↔ ¬b ≤ a := @right_lt_sup αᵒᵈ _ _ _
+
+theorem inf_lt_left_or_right (h : a ≠ b) : a ⊓ b < a ∨ a ⊓ b < b :=
+@left_or_right_lt_sup αᵒᵈ _ _ _ h
+
 theorem inf_of_le_right (h : b ≤ a) : a ⊓ b = b :=
 inf_eq_right.2 h
 
@@ -384,9 +387,6 @@ lemma inf_inf_distrib_left (a b c : α) : a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ (a ⊓
 lemma inf_inf_distrib_right (a b c : α) : (a ⊓ b) ⊓ c = (a ⊓ c) ⊓ (b ⊓ c) :=
 @sup_sup_distrib_right αᵒᵈ _ _ _ _
 
-lemma forall_le_or_exists_lt_inf (a : α) : (∀b, a ≤ b) ∨ (∃b, b < a) :=
-@forall_le_or_exists_lt_sup αᵒᵈ _ a
-
 theorem semilattice_inf.ext_inf {α} {A B : semilattice_inf α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y)
   (x y : α) : (by haveI := A; exact (x ⊓ y)) = x ⊓ y :=
@@ -406,10 +406,6 @@ theorem semilattice_inf.dual_dual (α : Type*) [H : semilattice_inf α] :
   order_dual.semilattice_inf αᵒᵈ = H :=
 semilattice_inf.ext $ λ _ _, iff.rfl
 
-theorem exists_lt_of_inf (α : Type*) [semilattice_inf α] [nontrivial α] :
-  ∃ a b : α, a < b :=
-let ⟨a, b, h⟩ := exists_lt_of_sup αᵒᵈ in ⟨b, a, h⟩
-
 lemma inf_le_ite (s s' : α) (P : Prop) [decidable P] : s ⊓ s' ≤ ite P s s' :=
 @ite_le_sup αᵒᵈ _ _ _ _ _
 

src/order/max.lean

@@ -184,14 +184,3 @@ protected lemma is_max.eq_of_le (ha : is_max a) (h : a ≤ b) : a = b := h.antis
 protected lemma is_max.eq_of_ge (ha : is_max a) (h : a ≤ b) : b = a := h.antisymm' $ ha h
 
 end partial_order
-
-section linear_order
-variables [linear_order α]
-
---TODO: Delete in favor of the directed version
-lemma is_top_or_exists_gt (a : α) : is_top a ∨ ∃ b, a < b :=
-by simpa only [or_iff_not_imp_left, is_top, not_forall, not_le] using id
-
-lemma is_bot_or_exists_lt (a : α) : is_bot a ∨ ∃ b, b < a := @is_top_or_exists_gt αᵒᵈ _ a
-
-end linear_order

src/topology/algebra/order/liminf_limsup.lean

@@ -22,10 +22,7 @@ section order_closed_topology
 variables [semilattice_sup α] [topological_space α] [order_topology α]
 
 lemma is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤) :=
-match forall_le_or_exists_lt_sup a with
-| or.inl h := ⟨a, eventually_of_forall h⟩
-| or.inr ⟨b, hb⟩ := ⟨b, ge_mem_nhds hb⟩
-end
+(is_top_or_exists_gt a).elim (λ h, ⟨a, eventually_of_forall h⟩) (λ ⟨b, hb⟩, ⟨b, ge_mem_nhds hb⟩)
 
 lemma filter.tendsto.is_bounded_under_le {f : filter β} {u : β → α} {a : α}
   (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≤) u :=