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