sup'_inv — Mathlib

English

For Finset s, Nonempty hs, and f, the variant sup' over s⁻¹ equals sup' over s after adjusting with inversion: sup' s⁻¹ hs f = sup' s hs.of_inv (f ·⁻¹).

Русский

Для Finset s, не пустого hs и функции f, вариант sup' по s⁻¹ равен sup' по s после применения инверсии к f.

LaTeX

$$$ \sup' s^{-1} \; hs \; f = \sup' s \; hs.of\_inv \; (f \cdot^{-1}) $$$

Lean4

@[to_additive (attr := simp)]
theorem sup'_inv [SemilatticeSup β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) :
    sup' s⁻¹ hs f = sup' s hs.of_inv (f ·⁻¹) :=
  sup'_image ..

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