[Merged by Bors] - feat: Extra sups lemmas

Mathlib/Data/Finset/Sups.lean

@@ -32,18 +32,16 @@ We define the following notation in locale `FinsetFamily`:
 [B. Bollobás, *Combinatorics*][bollobas1986]
 -/
 
-
 open Function
 
 open SetFamily
 
-variable {α : Type*} [DecidableEq α]
+variable {F α β : Type*} [DecidableEq α] [DecidableEq β]
 
 namespace Finset
 
 section Sups
-
-variable [SemilatticeSup α] (s s₁ s₂ t t₁ t₂ u v : Finset α)
+variable [SemilatticeSup α] [SemilatticeSup β] [SupHomClass F α β] (s s₁ s₂ t t₁ t₂ u v : Finset α)
 
 /-- `s ⊻ t` is the finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`. -/
 protected def hasSups : HasSups (Finset α) :=
@@ -178,6 +176,21 @@ theorem subset_sups {s t : Set α} :
   subset_image₂
 #align finset.subset_sups Finset.subset_sups
 
+lemma image_sups (f : F) (s t : Finset α) : image f (s ⊻ t) = image f s ⊻ image f t :=
+  image_image₂_distrib $ map_sup f
+
+lemma map_sups (f : F) (hf) (s t : Finset α) :
+    map ⟨f, hf⟩ (s ⊻ t) = map ⟨f, hf⟩ s ⊻ map ⟨f, hf⟩ t := by
+  simpa [map_eq_image] using image_sups f s t
+
+lemma subset_sups_self : s ⊆ s ⊻ s := fun _a ha ↦ mem_sups.2 ⟨_, ha, _, ha, sup_idem⟩
+lemma sups_subset_self : s ⊻ s ⊆ s ↔ SupClosed (s : Set α) := sups_subset_iff
+@[simp] lemma sups_eq_self : s ⊻ s = s ↔ SupClosed (s : Set α) := by simp [←coe_inj]
+
+lemma filter_sups_le [@DecidableRel α (· ≤ ·)] (s t : Finset α) (a : α) :
+    (s ⊻ t).filter (· ≤ a) = s.filter (· ≤ a) ⊻ t.filter (· ≤ a) := by
+  simp only [←coe_inj, coe_filter, coe_sups, ←mem_coe, Set.sep_sups_le]
+
 variable (s t u)
 
 theorem biUnion_image_sup_left : (s.biUnion fun a => t.image <| (· ⊔ ·) a) = s ⊻ t :=
@@ -216,8 +229,7 @@ theorem sups_sups_sups_comm : s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v) :=
 end Sups
 
 section Infs
-
-variable [SemilatticeInf α] (s s₁ s₂ t t₁ t₂ u v : Finset α)
+variable [SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] (s s₁ s₂ t t₁ t₂ u v : Finset α)
 
 /-- `s ⊼ t` is the finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`. -/
 protected def hasInfs : HasInfs (Finset α) :=
@@ -352,6 +364,21 @@ theorem subset_infs {s t : Set α} :
   subset_image₂
 #align finset.subset_infs Finset.subset_infs
 
+lemma image_infs (f : F) (s t : Finset α) : image f (s ⊼ t) = image f s ⊼ image f t :=
+  image_image₂_distrib $ map_inf f
+
+lemma map_infs (f : F) (hf) (s t : Finset α) :
+    map ⟨f, hf⟩ (s ⊼ t) = map ⟨f, hf⟩ s ⊼ map ⟨f, hf⟩ t := by
+  simpa [map_eq_image] using image_infs f s t
+
+lemma subset_infs_self : s ⊆ s ⊼ s := fun _a ha ↦ mem_infs.2 ⟨_, ha, _, ha, inf_idem⟩
+lemma infs_self_subset : s ⊼ s ⊆ s ↔ InfClosed (s : Set α) := infs_subset_iff
+@[simp] lemma infs_self : s ⊼ s = s ↔ InfClosed (s : Set α) := by simp [←coe_inj]
+
+lemma filter_infs_le [@DecidableRel α (· ≤ ·)] (s t : Finset α) (a : α) :
+    (s ⊼ t).filter (a ≤ ·) = s.filter (a ≤ ·) ⊼ t.filter (a ≤ ·) := by
+  simp only [←coe_inj, coe_filter, coe_infs, ←mem_coe, Set.sep_infs_le]
+
 variable (s t u)
 
 theorem biUnion_image_inf_left : (s.biUnion fun a => t.image <| (· ⊓ ·) a) = s ⊼ t :=
@@ -391,6 +418,22 @@ end Infs
 
 open FinsetFamily
 
+@[simp] lemma powerset_union (s t : Finset α) : (s ∪ t).powerset = s.powerset ⊻ t.powerset := by
+  ext u
+  simp only [mem_sups, mem_powerset, le_eq_subset, sup_eq_union]
+  refine ⟨fun h ↦ ⟨_, inter_subset_left _ u, _, inter_subset_left _ u, ?_⟩, ?_⟩
+  · rwa [←inter_distrib_right, inter_eq_right_iff_subset]
+  · rintro ⟨v, hv, w, hw, rfl⟩
+    exact union_subset_union hv hw
+
+@[simp] lemma powerset_inter (s t : Finset α) : (s ∩ t).powerset = s.powerset ⊼ t.powerset := by
+  ext u
+  simp only [mem_infs, mem_powerset, le_eq_subset, inf_eq_inter]
+  refine ⟨fun h ↦ ⟨_, inter_subset_left _ u, _, inter_subset_left _ u, ?_⟩, ?_⟩
+  · rwa [←inter_inter_distrib_right, inter_eq_right_iff_subset]
+  · rintro ⟨v, hv, w, hw, rfl⟩
+    exact inter_subset_inter hv hw
+
 section DistribLattice
 
 variable [DistribLattice α] (s t u : Finset α)

Mathlib/Data/Set/Sups.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Set.NAry
 import Mathlib.Order.UpperLower.Basic
+import Mathlib.Order.SupClosed
 
 #align_import data.set.sups from "leanprover-community/mathlib"@"20715f4ac6819ef2453d9e5106ecd086a5dc2a5e"
 
@@ -20,7 +21,7 @@ This file defines a few binary operations on `Set α` for use in set family comb
 
 ## Notation
 
-We define the following notation in locale `set_family`:
+We define the following notation in locale `SetFamily`:
 * `s ⊻ t`
 * `s ⊼ t`
 
@@ -32,7 +33,7 @@ We define the following notation in locale `set_family`:
 
 open Function
 
-variable {α : Type*}
+variable {F α β : Type*}
 
 /-- Notation typeclass for pointwise supremum `⊻`. -/
 class HasSups (α : Type*) where
@@ -45,8 +46,7 @@ class HasInfs (α : Type*) where
 #align has_infs HasInfs
 
 -- mathport name: «expr ⊻ »
-infixl:74
-  " ⊻ " => HasSups.sups
+infixl:74 " ⊻ " => HasSups.sups
   -- This notation is meant to have higher precedence than `⊔` and `⊓`, but still within the
   -- realm of other binary notation
 
@@ -56,8 +56,7 @@ infixl:75 " ⊼ " => HasInfs.infs
 namespace Set
 
 section Sups
-
-variable [SemilatticeSup α] (s s₁ s₂ t t₁ t₂ u v : Set α)
+variable [SemilatticeSup α] [SemilatticeSup β] [SupHomClass F α β] (s s₁ s₂ t t₁ t₂ u v : Set α)
 
 /-- `s ⊻ t` is the set of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`. -/
 protected def hasSups : HasSups (Set α) :=
@@ -170,6 +169,18 @@ theorem sups_inter_subset_right : s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻
   image2_inter_subset_right
 #align set.sups_inter_subset_right Set.sups_inter_subset_right
 
+lemma image_sups (f : F) (s t : Set α) : f '' (s ⊻ t) = f '' s ⊻ f '' t :=
+  image_image2_distrib $ map_sup f
+
+lemma subset_sups_self : s ⊆ s ⊻ s := λ _a ha ↦ mem_sups.2 ⟨_, ha, _, ha, sup_idem⟩
+lemma sups_subset_self : s ⊻ s ⊆ s ↔ SupClosed s := sups_subset_iff
+
+@[simp] lemma sups_eq_self : s ⊻ s = s ↔ SupClosed s :=
+  subset_sups_self.le.le_iff_eq.symm.trans sups_subset_self
+
+lemma sep_sups_le (s t : Set α) (a : α) :
+    {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a} := by ext; aesop
+
 variable (s t u)
 
 theorem iUnion_image_sup_left : ⋃ a ∈ s, (· ⊔ ·) a '' t = s ⊻ t :=
@@ -212,7 +223,7 @@ end Sups
 
 section Infs
 
-variable [SemilatticeInf α] (s s₁ s₂ t t₁ t₂ u v : Set α)
+variable [SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] (s s₁ s₂ t t₁ t₂ u v : Set α)
 
 /-- `s ⊼ t` is the set of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`. -/
 protected def hasInfs : HasInfs (Set α) :=
@@ -325,6 +336,18 @@ theorem infs_inter_subset_right : s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼
   image2_inter_subset_right
 #align set.infs_inter_subset_right Set.infs_inter_subset_right
 
+lemma image_infs (f : F) (s t : Set α) : f '' (s ⊼ t) = f '' s ⊼ f '' t :=
+  image_image2_distrib $ map_inf f
+
+lemma subset_infs_self : s ⊆ s ⊼ s := λ _a ha ↦ mem_infs.2 ⟨_, ha, _, ha, inf_idem⟩
+lemma infs_self_subset : s ⊼ s ⊆ s ↔ InfClosed s := infs_subset_iff
+
+@[simp] lemma infs_self : s ⊼ s = s ↔ InfClosed s :=
+  subset_infs_self.le.le_iff_eq.symm.trans infs_self_subset
+
+lemma sep_infs_le (s t : Set α) (a : α) :
+    {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b} := by ext; aesop
+
 variable (s t u)
 
 theorem iUnion_image_inf_left : ⋃ a ∈ s, (· ⊓ ·) a '' t = s ⊼ t :=

Mathlib/Order/SupClosed.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Christopher Hoskin
 -/
 import Mathlib.Data.Finset.Lattice
 import Mathlib.Order.Closure
+import Mathlib.Order.UpperLower.Basic
 
 /-!
 # Sets closed under join/meet
@@ -53,6 +54,8 @@ supClosed_sInter $ forall_range_iff.2 hf
 lemma SupClosed.directedOn (hs : SupClosed s) : DirectedOn (· ≤ ·) s :=
 λ _a ha _b hb ↦ ⟨_, hs ha hb, le_sup_left, le_sup_right⟩
 
+lemma IsUpperSet.supClosed (hs : IsUpperSet s) : SupClosed s := fun _a _ _b ↦ hs le_sup_right
+
 end Set
 
 section Finset
@@ -97,6 +100,8 @@ infClosed_sInter $ forall_range_iff.2 hf
 lemma InfClosed.codirectedOn (hs : InfClosed s) : DirectedOn (· ≥ ·) s :=
 λ _a ha _b hb ↦ ⟨_, hs ha hb, inf_le_left, inf_le_right⟩
 
+lemma IsLowerSet.infClosed (hs : IsLowerSet s) :  InfClosed s := λ _a _ _b ↦ hs inf_le_right
+
 end Set
 
 section Finset

Mathlib/Order/UpperLower/Basic.lean

@@ -1330,6 +1330,12 @@ theorem coe_lowerClosure (s : Set α) : ↑(lowerClosure s) = ⋃ a ∈ s, Iic a
   simp
 #align coe_lower_closure coe_lowerClosure
 
+instance instDecidablePredMemUpperClosure [DecidablePred (∃ a ∈ s, a ≤ ·)] :
+    DecidablePred (· ∈ upperClosure s) := ‹DecidablePred _›
+
+instance instDecidablePredMemLowerClosure [DecidablePred (∃ a ∈ s, · ≤ a)] :
+    DecidablePred (· ∈ lowerClosure s) := ‹DecidablePred _›
+
 theorem subset_upperClosure : s ⊆ upperClosure s := fun x hx => ⟨x, hx, le_rfl⟩
 #align subset_upper_closure subset_upperClosure