feat(order/lattice): add complete_semilattice_Sup/Inf (#6797)

This adds `complete_semilattice_Sup` and `complete_semilattice_Inf` above `complete_lattice`.

This has not much effect, as in fact either implies `complete_lattice`. However it's useful at times to have these, when you can naturally define just one half of the structure at a time (e.g. the subobject lattice in a general category, where for `Sup` we need coproducts and images, while for the `Inf` we need wide pullbacks).

There are many places in mathlib that currently use `complete_lattice_of_Inf`. It might be slightly nicer to instead construct a `complete_semilattice_Inf`, and then use the new `complete_lattice_of_complete_semilattice_Inf`, but I haven't done that here.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/real/ennreal.lean

@@ -1474,6 +1474,9 @@ section supr
 @[simp] lemma supr_eq_zero {ι : Sort*} {f : ι → ℝ≥0∞} : (⨆ i, f i) = 0 ↔ ∀ i, f i = 0 :=
 supr_eq_bot
 
+@[simp] lemma supr_zero_eq_zero {ι : Sort*} : (⨆ i : ι, (0 : ℝ≥0∞)) = 0 :=
+by simp
+
 lemma sup_eq_zero {a b : ℝ≥0∞} : a ⊔ b = 0 ↔ a = 0 ∧ b = 0 := sup_eq_bot_iff
 
 lemma supr_coe_nat : (⨆n:ℕ, (n : ℝ≥0∞)) = ∞ :=

src/measure_theory/measure_space.lean

@@ -804,6 +804,12 @@ have μ.to_outer_measure ≤ Inf (to_outer_measure '' m) :=
   le_Inf $ ball_image_of_ball $ assume μ hμ, to_outer_measure_le.2 $ h _ hμ,
 assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
 
+instance : complete_semilattice_Inf (measure α) :=
+{ Inf_le := λ s a, measure_Inf_le,
+  le_Inf := λ s a, measure_le_Inf,
+  ..(by apply_instance : partial_order (measure α)),
+  ..(by apply_instance : has_Inf (measure α)), }
+
 instance : complete_lattice (measure α) :=
 { bot := 0,
   bot_le := assume a s hs, by exact bot_le,
@@ -814,7 +820,7 @@ instance : complete_lattice (measure α) :=
     by cases s.eq_empty_or_nonempty with h  h;
       simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply],
 -/
-  .. complete_lattice_of_Inf (measure α) (λ ms, ⟨λ _, measure_Inf_le, λ _, measure_le_Inf⟩) }
+  .. complete_lattice_of_complete_semilattice_Inf (measure α) }
 
 end Inf
 
@@ -2078,9 +2084,9 @@ begin
         ennreal.sub_add_cancel_of_le (h₂ t h_t_measurable_set)] },
     have h_measure_sub_eq : (μ - ν) = measure_sub,
     { rw measure_theory.measure.sub_def, apply le_antisymm,
-      { apply @Inf_le (measure α) (measure.complete_lattice), simp [le_refl, add_comm,
+      { apply @Inf_le (measure α) measure.complete_semilattice_Inf, simp [le_refl, add_comm,
           h_measure_sub_add] },
-      apply @le_Inf (measure α) (measure.complete_lattice),
+      apply @le_Inf (measure α) measure.complete_semilattice_Inf,
       intros d h_d, rw [← h_measure_sub_add, mem_set_of_eq, add_comm d] at h_d,
       apply measure.le_of_add_le_add_left h_d },
     rw h_measure_sub_eq,

src/order/complete_lattice.lean

@@ -60,15 +60,91 @@ notation `⨅` binders `, ` r:(scoped f, infi f) := r
 instance (α) [has_Inf α] : has_Sup (order_dual α) := ⟨(Inf : set α → α)⟩
 instance (α) [has_Sup α] : has_Inf (order_dual α) := ⟨(Sup : set α → α)⟩
 
-/-- A complete lattice is a bounded lattice which
-  has suprema and infima for every subset. -/
-@[protect_proj]
-class complete_lattice (α : Type*) extends bounded_lattice α, has_Sup α, has_Inf α :=
+/--
+Note that we rarely use `complete_semilattice_Sup`
+(in fact, any such object is always a `complete_lattice`, so it's usually best to start there).
+
+Nevertheless it is sometimes a useful intermediate step in constructions.
+-/
+class complete_semilattice_Sup (α : Type*) extends partial_order α, has_Sup α :=
 (le_Sup : ∀s, ∀a∈s, a ≤ Sup s)
 (Sup_le : ∀s a, (∀b∈s, b ≤ a) → Sup s ≤ a)
+
+section
+variables [complete_semilattice_Sup α] {s t : set α} {a b : α}
+
+@[ematch] theorem le_Sup : a ∈ s → a ≤ Sup s := complete_semilattice_Sup.le_Sup s a
+
+theorem Sup_le : (∀b∈s, b ≤ a) → Sup s ≤ a := complete_semilattice_Sup.Sup_le s a
+
+lemma is_lub_Sup (s : set α) : is_lub s (Sup s) := ⟨assume x, le_Sup, assume x, Sup_le⟩
+
+lemma is_lub.Sup_eq (h : is_lub s a) : Sup s = a := (is_lub_Sup s).unique h
+
+theorem le_Sup_of_le (hb : b ∈ s) (h : a ≤ b) : a ≤ Sup s :=
+le_trans h (le_Sup hb)
+
+theorem Sup_le_Sup (h : s ⊆ t) : Sup s ≤ Sup t :=
+(is_lub_Sup s).mono (is_lub_Sup t) h
+
+@[simp] theorem Sup_le_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
+is_lub_le_iff (is_lub_Sup s)
+
+theorem Sup_le_Sup_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) : Sup s ≤ Sup t :=
+le_of_forall_le' (by simp only [Sup_le_iff]; introv h₀ h₁; rcases h _ h₁ with ⟨y,hy,hy'⟩; solve_by_elim [le_trans hy'])
+
+-- We will generalize this to conditionally complete lattices in `cSup_singleton`.
+theorem Sup_singleton {a : α} : Sup {a} = a :=
+is_lub_singleton.Sup_eq
+
+end
+
+/--
+Note that we rarely use `complete_semilattice_Inf`
+(in fact, any such object is always a `complete_lattice`, so it's usually best to start there).
+
+Nevertheless it is sometimes a useful intermediate step in constructions.
+-/
+class complete_semilattice_Inf (α : Type*) extends partial_order α, has_Inf α :=
 (Inf_le : ∀s, ∀a∈s, Inf s ≤ a)
 (le_Inf : ∀s a, (∀b∈s, a ≤ b) → a ≤ Inf s)
 
+
+section
+variables [complete_semilattice_Inf α] {s t : set α} {a b : α}
+
+@[ematch] theorem Inf_le : a ∈ s → Inf s ≤ a := complete_semilattice_Inf.Inf_le s a
+
+theorem le_Inf : (∀b∈s, a ≤ b) → a ≤ Inf s := complete_semilattice_Inf.le_Inf s a
+
+lemma is_glb_Inf (s : set α) : is_glb s (Inf s) := ⟨assume a, Inf_le, assume a, le_Inf⟩
+
+lemma is_glb.Inf_eq (h : is_glb s a) : Inf s = a := (is_glb_Inf s).unique h
+
+theorem Inf_le_of_le (hb : b ∈ s) (h : b ≤ a) : Inf s ≤ a :=
+le_trans (Inf_le hb) h
+
+theorem Inf_le_Inf (h : s ⊆ t) : Inf t ≤ Inf s :=
+(is_glb_Inf s).mono (is_glb_Inf t) h
+
+@[simp] theorem le_Inf_iff : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
+le_is_glb_iff (is_glb_Inf s)
+
+theorem Inf_le_Inf_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) : Inf t ≤ Inf s :=
+le_of_forall_le (by simp only [le_Inf_iff]; introv h₀ h₁; rcases h _ h₁ with ⟨y,hy,hy'⟩; solve_by_elim [le_trans _ hy'])
+
+-- We will generalize this to conditionally complete lattices in `cInf_singleton`.
+theorem Inf_singleton {a : α} : Inf {a} = a :=
+is_glb_singleton.Inf_eq
+
+end
+
+/-- A complete lattice is a bounded lattice which
+  has suprema and infima for every subset. -/
+@[protect_proj]
+class complete_lattice (α : Type*) extends
+  bounded_lattice α, complete_semilattice_Sup α, complete_semilattice_Inf α.
+
 /-- Create a `complete_lattice` from a `partial_order` and `Inf` function
 that returns the greatest lower bound of a set. Usually this constructor provides
 poor definitional equalities.  If other fields are known explicitly, they should be
@@ -106,6 +182,16 @@ def complete_lattice_of_Inf (α : Type*) [H1 : partial_order α]
   Sup_le := λ s a ha, (is_glb_Inf (upper_bounds s)).1 ha,
   .. H1, .. H2 }
 
+/--
+Any `complete_semilattice_Inf` is in fact a `complete_lattice`.
+
+Note that this construction has bad definitional properties:
+see the doc-string on `complete_lattice_of_Inf`.
+-/
+def complete_lattice_of_complete_semilattice_Inf (α : Type*) [complete_semilattice_Inf α] :
+  complete_lattice α :=
+complete_lattice_of_Inf α (λ s, is_glb_Inf s)
+
 /-- Create a `complete_lattice` from a `partial_order` and `Sup` function
 that returns the least upper bound of a set. Usually this constructor provides
 poor definitional equalities.  If other fields are known explicitly, they should be
@@ -143,6 +229,16 @@ def complete_lattice_of_Sup (α : Type*) [H1 : partial_order α]
   le_Inf := λ s a ha, (is_lub_Sup (lower_bounds s)).1 ha,
   .. H1, .. H2 }
 
+/--
+Any `complete_semilattice_Sup` is in fact a `complete_lattice`.
+
+Note that this construction has bad definitional properties:
+see the doc-string on `complete_lattice_of_Sup`.
+-/
+def complete_lattice_of_complete_semilattice_Sup (α : Type*) [complete_semilattice_Sup α] :
+  complete_lattice α :=
+complete_lattice_of_Sup α (λ s, is_lub_Sup s)
+
 /-- A complete linear order is a linear order whose lattice structure is complete. -/
 class complete_linear_order (α : Type*) extends complete_lattice α, linear_order α
 
@@ -164,50 +260,9 @@ end order_dual
 section
 variables [complete_lattice α] {s t : set α} {a b : α}
 
-@[ematch] theorem le_Sup : a ∈ s → a ≤ Sup s := complete_lattice.le_Sup s a
-
-theorem Sup_le : (∀b∈s, b ≤ a) → Sup s ≤ a := complete_lattice.Sup_le s a
-
-@[ematch] theorem Inf_le : a ∈ s → Inf s ≤ a := complete_lattice.Inf_le s a
-
-theorem le_Inf : (∀b∈s, a ≤ b) → a ≤ Inf s := complete_lattice.le_Inf s a
-
-lemma is_lub_Sup (s : set α) : is_lub s (Sup s) := ⟨assume x, le_Sup, assume x, Sup_le⟩
-
-lemma is_lub.Sup_eq (h : is_lub s a) : Sup s = a := (is_lub_Sup s).unique h
-
-lemma is_glb_Inf (s : set α) : is_glb s (Inf s) := ⟨assume a, Inf_le, assume a, le_Inf⟩
-
-lemma is_glb.Inf_eq (h : is_glb s a) : Inf s = a := (is_glb_Inf s).unique h
-
-theorem le_Sup_of_le (hb : b ∈ s) (h : a ≤ b) : a ≤ Sup s :=
-le_trans h (le_Sup hb)
-
-theorem Inf_le_of_le (hb : b ∈ s) (h : b ≤ a) : Inf s ≤ a :=
-le_trans (Inf_le hb) h
-
-theorem Sup_le_Sup (h : s ⊆ t) : Sup s ≤ Sup t :=
-(is_lub_Sup s).mono (is_lub_Sup t) h
-
-theorem Inf_le_Inf (h : s ⊆ t) : Inf t ≤ Inf s :=
-(is_glb_Inf s).mono (is_glb_Inf t) h
-
-@[simp] theorem Sup_le_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
-is_lub_le_iff (is_lub_Sup s)
-
-@[simp] theorem le_Inf_iff : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
-le_is_glb_iff (is_glb_Inf s)
-
-theorem Sup_le_Sup_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) : Sup s ≤ Sup t :=
-le_of_forall_le' (by simp only [Sup_le_iff]; introv h₀ h₁; rcases h _ h₁ with ⟨y,hy,hy'⟩; solve_by_elim [le_trans hy'])
-
-theorem Inf_le_Inf_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) : Inf t ≤ Inf s :=
-le_of_forall_le (by simp only [le_Inf_iff]; introv h₀ h₁; rcases h _ h₁ with ⟨y,hy,hy'⟩; solve_by_elim [le_trans _ hy'])
-
 theorem Inf_le_Sup (hs : s.nonempty) : Inf s ≤ Sup s :=
 is_glb_le_is_lub (is_glb_Inf s) (is_lub_Sup s) hs
 
--- TODO: it is weird that we have to add union_def
 theorem Sup_union {s t : set α} : Sup (s ∪ t) = Sup s ⊔ Sup t :=
 ((is_lub_Sup s).union (is_lub_Sup t)).Sup_eq
 
@@ -224,7 +279,7 @@ theorem le_Inf_inter {s t : set α} : Inf s ⊔ Inf t ≤ Inf (s ∩ t) :=
 @Sup_inter_le (order_dual α) _ _ _
 
 @[simp] theorem Sup_empty : Sup ∅ = (⊥ : α) :=
-is_lub_empty.Sup_eq
+(@is_lub_empty α _).Sup_eq
 
 @[simp] theorem Inf_empty : Inf ∅ = (⊤ : α) :=
 (@is_glb_empty α _).Inf_eq
@@ -233,7 +288,7 @@ is_lub_empty.Sup_eq
 (@is_lub_univ α _).Sup_eq
 
 @[simp] theorem Inf_univ : Inf univ = (⊥ : α) :=
-is_glb_univ.Inf_eq
+(@is_glb_univ α _).Inf_eq
 
 -- TODO(Jeremy): get this automatically
 @[simp] theorem Sup_insert {a : α} {s : set α} : Sup (insert a s) = a ⊔ Sup s :=
@@ -248,14 +303,6 @@ le_trans (Sup_le_Sup h) (le_of_eq (trans Sup_insert bot_sup_eq))
 theorem Inf_le_Inf_of_subset_insert_top (h : s ⊆ insert ⊤ t) : Inf t ≤ Inf s :=
 le_trans (le_of_eq (trans top_inf_eq.symm Inf_insert.symm)) (Inf_le_Inf h)
 
--- We will generalize this to conditionally complete lattices in `cSup_singleton`.
-theorem Sup_singleton {a : α} : Sup {a} = a :=
-is_lub_singleton.Sup_eq
-
--- We will generalize this to conditionally complete lattices in `cInf_singleton`.
-theorem Inf_singleton {a : α} : Inf {a} = a :=
-is_glb_singleton.Inf_eq
-
 theorem Sup_pair {a b : α} : Sup {a, b} = a ⊔ b :=
 (@is_lub_pair α _ a b).Sup_eq
 

src/topology/instances/ennreal.lean

@@ -394,7 +394,7 @@ begin
     simpa [add_supr, supr_add] using
       λ i j:ι, show f i + g j ≤ ⨆ a, f a + g a, from
       let ⟨k, hk⟩ := h i j in le_supr_of_le k hk },
-  { have : ∀f:ι → ℝ≥0∞, (⨆i, f i) = 0 := λ f, bot_unique (supr_le $ assume i, (hι ⟨i⟩).elim),
+  { have : ∀f:ι → ℝ≥0∞, (⨆i, f i) = 0 := λ f, supr_eq_zero.mpr (λ i, (hι ⟨i⟩).elim),
     rw [this, this, this, zero_add] }
 end
 
@@ -408,8 +408,7 @@ lemma finset_sum_supr_nat {α} {ι} [semilattice_sup ι] {s : finset α} {f : α
   ∑ a in s, supr (f a) = (⨆ n, ∑ a in s, f a n) :=
 begin
   refine finset.induction_on s _ _,
-  { simp,
-    exact (bot_unique $ supr_le $ assume i, le_refl ⊥).symm },
+  { simp, },
   { assume a s has ih,
     simp only [finset.sum_insert has],
     rw [ih, supr_add_supr_of_monotone (hf a)],

src/topology/omega_complete_partial_order.lean

@@ -139,8 +139,9 @@ begin
   cases hf, specialize hf_h c,
   simp only [not_below, preorder_hom.coe_fun_mk, eq_iff_iff, set.mem_set_of_eq] at hf_h,
   rw [← not_iff_not],
-  simp only [ωSup_le_iff, hf_h, ωSup, supr, Sup, complete_lattice.Sup, exists_prop, set.mem_range,
-    preorder_hom.coe_fun_mk, chain.map_to_fun, function.comp_app, eq_iff_iff, not_forall],
+  simp only [ωSup_le_iff, hf_h, ωSup, supr, Sup, complete_lattice.Sup, complete_semilattice_Sup.Sup,
+    exists_prop, set.mem_range, preorder_hom.coe_fun_mk, chain.map_to_fun, function.comp_app,
+    eq_iff_iff, not_forall],
   tauto,
 end