sup_disjSum — Mathlib

English

The supremum over a disjoint sum of two finset-indexed families equals the join of the two corresponding disjoint parts: sup over inl and sup over inr.

Русский

Супремум над объединением через дизъюнкцию двух семейств равен объединению двух соответствующих частей: sup над inl и sup над inr.

LaTeX

$$$(s.disjSum t).sup f = \bigl( s.sup (\lambda x. f (Sum.inl x))\bigr) \;\lor\; (t.sup (\lambda x. f (Sum.inr x)))$$$

Lean4

@[simp]
theorem sup_disjSum (s : Finset β) (t : Finset γ) (f : β ⊕ γ → α) :
    (s.disjSum t).sup f = (s.sup fun x ↦ f (.inl x)) ⊔ (t.sup fun x ↦ f (.inr x)) :=
  congr(fold _ $(bot_sup_eq _ |>.symm) _ _).trans (fold_disjSum _ _ _ _ _ _)

Похожие утверждения