inf_sdiff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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