inf_himp_right — Mathlib

English

In a Boolean algebra, for Finset s and function f, the infimum of f b ⇨ a over b in s equals the implication of the supremum of f with a: (s.inf (fun b => f b ⇨ a)) = (s.sup f) ⇨ a.

Русский

В булевой алгебре для Finset s и функции f справедливо равенство: inf b∈s (f b ⇨ a) = (sup b∈s f b) ⇨ a.

LaTeX

$$Eq (s.inf (fun b => inst.himp (f b) a)) (inst.himp (s.sup f) a)$$

Lean4

theorem inf_himp_right (s : Finset ι) (f : ι → α) (a : α) : (s.inf fun b => f b ⇨ a) = s.sup f ⇨ a :=
  @sup_sdiff_left αᵒᵈ _ _ _ _ _

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