inf_sdiff_left — Mathlib

English

In a Boolean algebra, for a nonempty finite set s, the infimum over i ∈ s of a \ f(i) equals a \ (sup over i ∈ s of f(i)).

Русский

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

LaTeX

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

Lean4

theorem inf_sdiff_left (hs : s.Nonempty) (f : ι → α) (a : α) : (s.inf fun b => a \ f b) = a \ s.sup f := by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [sup_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [sup_cons, inf_cons, ih, sdiff_sup]

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