sup_sdiff_right — Mathlib

English

In a generalized Boolean algebra, the supremum distributes over the right-sdifferential operation: sup_b (f(b) \ a) = (sup_b f(b)) \ a.

Русский

В обобщённой булевой алгебре объединение через справа-дивидент сохраняет операцию разности: sup_b (f(b) \ a) = (sup_b f(b)) \ a.

LaTeX

$$$\displaystyle (s.\sup (\lambda b. f b \setminus a)) = s.sup f \setminus a$$$

Lean4

theorem sup_sdiff_right {α β : Type*} [GeneralizedBooleanAlgebra α] (s : Finset β) (f : β → α) (a : α) :
    (s.sup fun b => f b \ a) = s.sup f \ a := by
  induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, bot_sdiff]
  | cons _ _ _ h => rw [sup_cons, sup_cons, h, sup_sdiff]

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