English
Let α be a distributive lattice. For s Nonempty and t with each t b Nonempty, we have\n\\[ (s.biUnion t).sup' (Hs.biUnion fun b _ => Ht b) f = s.sup' Hs (fun b => (t b).sup' (Ht b) f). \\]
Русский
Пусть α — дистрибутивная решётка. Пусть s непусто, и для каждого b множество t(b) непусто. Тогда\n\\[ (s.biUnion t).sup' (Hs.biUnion ...) f = s.sup' Hs (λ b, (t b).sup' (Ht b) f). \\]
LaTeX
$$$$ (s.biUnion t)^{\\sup'} (Hs.biUnion (\\cdot) (Ht)) f = s^{\\sup'} Hs (\\lambda b, (t b)^{\\sup'} (Ht b) f). $$$$
Lean4
theorem sup'_biUnion [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ b, (t b).Nonempty) :
(s.biUnion t).sup' (Hs.biUnion fun b _ => Ht b) f = s.sup' Hs (fun b => (t b).sup' (Ht b) f) :=
eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]
