sup_himp_left — Mathlib

English

For a nonempty finite s, the supremum of a ⇒ f(i) over i ∈ s equals a ⇒ (sup f).

Русский

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

LaTeX

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

Lean4

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

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