sup'_image — Mathlib

English

For s finite and f: γ → β with nonempty image, the supremum over the image with g equals the supremum over s of g ∘ f.

Русский

Для конечного s и отображения f: γ → β, при непустом образе, sup' образа равен sup' над s от g∘f.

LaTeX

$$$ (s.image f).sup' hs g = s.sup' hs.of_image (g \circ f)$$$

Lean4

/-- To rewrite from right to left, use `Finset.sup'_comp_eq_image`. -/
@[simp]
theorem sup'_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (s.image f).Nonempty) (g : β → α) :
    (s.image f).sup' hs g = s.sup' hs.of_image (g ∘ f) := by rw [← WithBot.coe_eq_coe]; simp only [coe_sup', sup_image];
  rfl

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