Commit 2025-03-20 09:52 f3beb9c2
View on Github →feat(Data/Finset/Sum): supremum over a disjoint union (#22983)
Add sup_disjSum and inf_disjSum.
sup_disjSum:
(s.disjSum t).sup f = (s.sup fun x ↦ f (Sum.inl x)) ⊔ (t.sup fun x ↦ f (Sum.inr x))
inf_disjSum:
(s.disjSum t).inf f = (s.inf fun x ↦ f (Sum.inl x)) ⊓ (t.inf fun x ↦ f (Sum.inr x))