English
Let α be a distributive lattice. For a finite s ⊆ γ, with Hs : s.Nonempty and t : γ → Finset β with Ht b : (t b).Nonempty for all b, 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 непустое Finset γ, а t: γ → Finset β таково, что (t b) непусто для каждого b. Тогда\n\\[ (s.biUnion t).sup' (Hs.biUnion fun b _ => Ht b) f = s.sup' Hs (fun 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
@[simp]
theorem sup_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
(s.biUnion t).sup f = s.sup fun x => (t x).sup f :=
eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]
