sup_himp_right — Mathlib

English

For a nonempty finite set s in a Boolean algebra, the supremum of f(i) ⇒ a over i ∈ s equals (inf f) ⇒ a.

Русский

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

LaTeX

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

Lean4

theorem sup_himp_right (hs : s.Nonempty) (f : ι → α) (a : α) : (s.sup fun b => f b ⇨ a) = s.inf f ⇨ a :=
  @inf_sdiff_left αᵒᵈ _ _ _ hs _ _

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