feat(order/closure): closure of unions and bUnions (#7361)

prove closure_closure_union and similar

src/order/closure.lean

@@ -26,7 +26,7 @@ by coercion, see `closure_operator.gi`.
 * https://en.wikipedia.org/wiki/Closure_operator#Closure_operators_on_partially_ordered_sets
 
 -/
-universe u
+universes u v
 
 variables (α : Type u) [partial_order α]
 
@@ -73,25 +73,58 @@ def mk' (f : α → α) (hf₁ : monotone f) (hf₂ : ∀ x, x ≤ f x) (hf₃ :
   le_closure' := hf₂,
   idempotent' := λ x, le_antisymm (hf₃ x) (hf₁ (hf₂ x)) }
 
+/-- Convenience constructor for a closure operator using the weaker minimality axiom:
+`x ≤ f y → f x ≤ f y`, which is sometimes easier to prove in practice. -/
+@[simps]
+def mk₂ (f : α → α) (hf : ∀ x, x ≤ f x) (hmin : ∀ ⦃x y⦄, x ≤ f y → f x ≤ f y) :
+  closure_operator α :=
+{ to_fun := f,
+  monotone' := λ x y hxy, hmin (le_trans hxy (hf y)),
+  le_closure' := hf,
+  idempotent' := λ x, le_antisymm (hmin (le_refl _)) (hf _) }
+
+/-- Expanded out version of `mk₂`. `p` implies being closed. This constructor should be used when
+you already know a sufficient condition for being closed and using `mem_mk₃_closed` will avoid you
+the (slight) hassle of having to prove it both inside and outside the constructor. -/
+@[simps]
+def mk₃ (f : α → α) (p : α → Prop) (hf : ∀ x, x ≤ f x) (hfp : ∀ x, p (f x))
+  (hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y) :
+  closure_operator α :=
+mk₂ f hf (λ x y hxy, hmin hxy (hfp y))
+
+/-- This lemma shows that the image of `x` of a closure operator built from the `mk₃` constructor
+respects `p`, the property that was fed into it. -/
+lemma closure_mem_mk₃ {f : α → α} {p : α → Prop} {hf : ∀ x, x ≤ f x} {hfp : ∀ x, p (f x)}
+  {hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y} (x : α) :
+  p (mk₃ f p hf hfp hmin x) :=
+hfp x
+
+/-- Analogue of `closure_le_closed_iff_le` but with the `p` that was fed into the `mk₃` constructor.
+-/
+lemma closure_le_mk₃_iff {f : α → α} {p : α → Prop} {hf : ∀ x, x ≤ f x} {hfp : ∀ x, p (f x)}
+  {hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y} {x y : α} (hxy : x ≤ y) (hy : p y) :
+  mk₃ f p hf hfp hmin x ≤ y :=
+hmin hxy hy
+
 @[mono] lemma monotone : monotone c := c.monotone'
 /--
 Every element is less than its closure. This property is sometimes referred to as extensivity or
-inflationary.
+inflationarity.
 -/
 lemma le_closure (x : α) : x ≤ c x := c.le_closure' x
 @[simp] lemma idempotent (x : α) : c (c x) = c x := c.idempotent' x
 
 lemma le_closure_iff (x y : α) : x ≤ c y ↔ c x ≤ c y :=
 ⟨λ h, c.idempotent y ▸ c.monotone h, λ h, le_trans (c.le_closure x) h⟩
 
-lemma closure_top {α : Type u} [order_top α] (c : closure_operator α) : c ⊤ = ⊤ :=
+@[simp] lemma closure_top {α : Type u} [order_top α] (c : closure_operator α) : c ⊤ = ⊤ :=
 le_antisymm le_top (c.le_closure _)
 
-lemma closure_inter_le {α : Type u} [semilattice_inf α] (c : closure_operator α) (x y : α) :
+lemma closure_inf_le {α : Type u} [semilattice_inf α] (c : closure_operator α) (x y : α) :
   c (x ⊓ y) ≤ c x ⊓ c y :=
 c.monotone.map_inf_le _ _
 
-lemma closure_union_closure_le {α : Type u} [semilattice_sup α] (c : closure_operator α) (x y : α) :
+lemma closure_sup_closure_le {α : Type u} [semilattice_sup α] (c : closure_operator α) (x y : α) :
   c x ⊔ c y ≤ c (x ⊔ y) :=
 c.monotone.le_map_sup _ _
 
@@ -115,13 +148,54 @@ def to_closed (x : α) : c.closed := ⟨c x, c.closure_is_closed x⟩
 lemma top_mem_closed {α : Type u} [order_top α] (c : closure_operator α) : ⊤ ∈ c.closed :=
 c.closure_top
 
-lemma closure_le_closed_iff_le {x y : α} (hy : c.closed y) : x ≤ y ↔ c x ≤ y :=
-by rw [← c.closure_eq_self_of_mem_closed hy, le_closure_iff]
+@[simp] lemma closure_le_closed_iff_le (x : α) {y : α} (hy : c.closed y) : c x ≤ y ↔ x ≤ y :=
+by rw [←c.closure_eq_self_of_mem_closed hy, ←le_closure_iff]
+
+/-- A closure operator is equal to the closure operator obtained by feeding `c.closed` into the
+`mk₃` constructor. -/
+lemma eq_mk₃_closed (c : closure_operator α) :
+  c = mk₃ c c.closed c.le_closure c.closure_is_closed
+  (λ x y hxy hy, (c.closure_le_closed_iff_le x hy).2 hxy) :=
+by { ext, refl }
+
+/-- This lemma shows that the `p` fed into the `mk₃` constructor implies being closed. -/
+lemma mem_mk₃_closed {f : α → α} {p : α → Prop} {hf : ∀ x, x ≤ f x} {hfp : ∀ x, p (f x)}
+  {hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y} {x : α} (hx : p x) :
+  x ∈ (mk₃ f p hf hfp hmin).closed :=
+le_antisymm (hmin (le_refl _) hx) (hf _)
+
+@[simp] lemma closure_sup_closure_left {α : Type u} [semilattice_sup α] (c : closure_operator α)
+  (x y : α) :
+  c (c x ⊔ y) = c (x ⊔ y) :=
+le_antisymm ((le_closure_iff c _ _).1 (sup_le (c.monotone le_sup_left)
+  (le_trans le_sup_right (le_closure _ _)))) (c.monotone (sup_le_sup_right (le_closure _ _) _))
+
+@[simp] lemma closure_sup_closure_right {α : Type u} [semilattice_sup α] (c : closure_operator α)
+  (x y : α) :
+  c (x ⊔ c y) = c (x ⊔ y) :=
+by rw [sup_comm, closure_sup_closure_left, sup_comm]
+
+@[simp] lemma closure_sup_closure {α : Type u} [semilattice_sup α] (c : closure_operator α)
+  (x y : α) :
+  c (c x ⊔ c y) = c (x ⊔ y) :=
+by rw [closure_sup_closure_left, closure_sup_closure_right]
+
+@[simp] lemma closure_supr_closure {α : Type u} {ι : Type v} [complete_lattice α]
+  (c : closure_operator α) (x : ι → α) :
+  c (⨆ i, c (x i)) = c (⨆ i, x i) :=
+le_antisymm ((le_closure_iff c _ _).1 (supr_le (λ i, c.monotone
+  (le_supr _ _)))) (c.monotone (supr_le_supr (λ i, c.le_closure _)))
+
+@[simp] lemma closure_bsupr_closure {α : Type u} [complete_lattice α] (c : closure_operator α)
+  (p : α → Prop) :
+  c (⨆ x (H : p x), c x) = c (⨆ x (H : p x), x) :=
+le_antisymm ((le_closure_iff c _ _).1 (bsupr_le (λ x hx, c.monotone
+  (le_bsupr_of_le x hx (le_refl x))))) (c.monotone (bsupr_le_bsupr (λ x hx, le_closure _ _)))
 
 /-- The set of closed elements has a Galois insertion to the underlying type. -/
 def gi : galois_insertion c.to_closed coe :=
 { choice := λ x hx, ⟨x, le_antisymm hx (c.le_closure x)⟩,
-  gc := λ x y, (c.closure_le_closed_iff_le y.2).symm,
+  gc := λ x y, (c.closure_le_closed_iff_le _ y.2),
   le_l_u := λ x, c.le_closure _,
   choice_eq := λ x hx, le_antisymm (c.le_closure x) hx }
 

src/order/complete_lattice.lean

@@ -315,7 +315,7 @@ theorem le_Inf_inter {s t : set α} : Inf s ⊔ Inf t ≤ Inf (s ∩ t) :=
 @[simp] theorem Inf_insert {a : α} {s : set α} : Inf (insert a s) = a ⊓ Inf s :=
 ((is_glb_Inf s).insert a).Inf_eq
 
-theorem Sup_le_Sup_of_subset_instert_bot (h : s ⊆ insert ⊥ t) : Sup s ≤ Sup t :=
+theorem Sup_le_Sup_of_subset_insert_bot (h : s ⊆ insert ⊥ t) : Sup s ≤ Sup t :=
 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 :=