English
Let s and t be finite sets and f on their disjoint union. Then (s ⊎ t).inf f equals the meet of s.inf (f ∘ inl) and t.inf (f ∘ inr).
Русский
Пусть s и t — конечные множества и функция f над их попарно-дисъюнктным объединением. Тогда inf по s ⊎ t от f равен наименьшему элементу двух инфимуумов: inf_s f∘inl и inf_t f∘inr.
LaTeX
$$$ (s\\disjSum t).inf f = (s.inf (\\lambda x, f(\\mathrm{inl} x))) \\inf (t.inf (\\lambda x, f(\\mathrm{inr} x))) $$$
Lean4
@[simp]
theorem inf_disjSum (s : Finset β) (t : Finset γ) (f : β ⊕ γ → α) :
(s.disjSum t).inf f = (s.inf fun x ↦ f (.inl x)) ⊓ (t.inf fun x ↦ f (.inr x)) :=
congr(fold _ $(top_inf_eq _ |>.symm) _ _).trans (fold_disjSum _ _ _ _ _ _)
