feat(algebra/pointwise): add partial order to set_semiring (#11567)

This PR introduces the natural inclusion order on sets on `set_semiring`.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Ordered.20semirings)



Co-authored-by: Damiano Testa <maskal@CLD-E854D68C.ads.warwick.ac.uk>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/pointwise.lean

@@ -812,7 +812,7 @@ section monoid
 
 /-- An alias for `set α`, which has a semiring structure given by `∪` as "addition" and pointwise
   multiplication `*` as "multiplication". -/
-@[derive inhabited] def set_semiring (α : Type*) : Type* := set α
+@[derive [inhabited, partial_order, order_bot]] def set_semiring (α : Type*) : Type* := set α
 
 /-- The identitiy function `set α → set_semiring α`. -/
 protected def up (s : set α) : set_semiring α := s
@@ -821,6 +821,14 @@ protected def set_semiring.down (s : set_semiring α) : set α := s
 @[simp] protected lemma down_up {s : set α} : s.up.down = s := rfl
 @[simp] protected lemma up_down {s : set_semiring α} : s.down.up = s := rfl
 
+/- This lemma is not tagged `simp`, since otherwise the linter complains. -/
+lemma up_le_up {s t : set α} : s.up ≤ t.up ↔ s ⊆ t := iff.rfl
+/- This lemma is not tagged `simp`, since otherwise the linter complains. -/
+lemma up_lt_up {s t : set α} : s.up < t.up ↔ s ⊂ t := iff.rfl
+
+@[simp] lemma down_subset_down {s t : set_semiring α} : s.down ⊆ t.down ↔ s ≤ t := iff.rfl
+@[simp] lemma down_ssubset_down {s t : set_semiring α} : s.down ⊂ t.down ↔ s < t := iff.rfl
+
 instance set_semiring.add_comm_monoid : add_comm_monoid (set_semiring α) :=
 { add := λ s t, (s ∪ t : set α),
   zero := (∅ : set α),