English
Let α be a distributive lattice with Inf. For finite s ⊆ γ, with Hs : s.Nonempty and t : γ → Finset β with Ht b : (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). \\]
Русский
Пусть α — дистрибутивная решётка с Inf. Пусть s непусто, t: γ → Finset β, и каждый 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 f) f = s^{\\inf'} Hs (\\lambda b, (t b)^{\\inf'} (Ht b) f). $$$$
Lean4
@[simp]
theorem inf_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
(s.biUnion t).inf f = s.inf fun x => (t x).inf f :=
@sup_biUnion αᵒᵈ _ _ _ _ _ _ _ _
