sup'_comp_eq_image — Mathlib

English

A counterpart of sup'_image: sup' over s by g ∘ f equals the supremum over the image of s under f.

Русский

Противоположный вариант sup'_image: sup' по g∘f равно sup' по изображению s через f.

LaTeX

$$$\text{sup' } s \; (\mathrm{comp}\ g\ f) = (\mathrm{image}\ f\ s).sup' \; (\mathrm{of_image}\ f)\ g$$$

Lean4

/-- A version of `Finset.sup'_image` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty. -/
theorem sup'_comp_eq_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : s.Nonempty) (g : β → α) :
    s.sup' hs (g ∘ f) = (s.image f).sup' (hs.image f) g :=
  .symm <| sup'_image _ _

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