English
Distributivity of inf over finite supremum from the left: a ∧ (s.sup f) = s.sup (a ∧ f i).
Русский
Распространение инфа по левому аргументу над конечной объединением: a ∧ (s.sup f) = s.sup (a ∧ f i).
LaTeX
$$$ a \\wedge s.\\sup f = s.\\sup (\\\\lambda i, a \\wedge f i) $$$
Lean4
theorem sup_inf_distrib_left (s : Finset ι) (f : ι → α) (a : α) : a ⊓ s.sup f = s.sup fun i => a ⊓ f i := by
induction s using Finset.cons_induction with
| empty => simp_rw [Finset.sup_empty, inf_bot_eq]
| cons _ _ _ h => rw [sup_cons, sup_cons, inf_sup_left, h]