sup'_union — Mathlib

English

For nonempty Finsets s1, s2 and f, the supremum over the union equals the join of the supremums: (s1 ∪ s2).sup' f = s1.sup' f ⊔ s2.sup' f.

Русский

Для непустых Finset s1, s2 и отображения f: β → α, sup' по объединению равен объединению двух supremums.

LaTeX

$$$(s_1 \cup s_2).sup' (\,f\,) = s_1.sup' f \;⊔\; s_2.sup' f$$$

Lean4

theorem sup'_union [DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : β → α) :
    (s₁ ∪ s₂).sup' (h₁.mono subset_union_left) f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f :=
  eq_of_forall_ge_iff fun a => by simp [or_imp, forall_and]

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