sup_inf_distrib_left — Mathlib

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]

Похожие утверждения