sup_sdiff_left — Mathlib

English

In a Boolean algebra, for any finite set s and function f, the supremum over s of a \ f(i) equals a \ (inf over s of f(i)).

Русский

В булевой алгебре для любой конечной множности s и функции f выполняется тождество: \\bigvee_{i∈s} (a \ f(i)) = a \bigwedge_{i∈s} f(i).

LaTeX

$$$\bigvee_{b\in s} (a \ f(b)) = a \\ s\inf f$$$

Lean4

theorem sup_sdiff_left (s : Finset ι) (f : ι → α) (a : α) : (s.sup fun b => a \ f b) = a \ s.inf f := by
  induction s using Finset.cons_induction with
  | empty => rw [sup_empty, inf_empty, sdiff_top]
  | cons _ _ _ h => rw [sup_cons, inf_cons, h, sdiff_inf]

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