sup_inv — Mathlib

English

For Finset s and function f, the supremum over s⁻¹ of f equals the supremum over s of f composed with inversion: sup s⁻¹ f = sup s (f ∘ inv).

Русский

Для Finset s и функции f верхняя граница по s⁻¹ равна верхней границе по s от f ∘ инверсия.

LaTeX

$$$ \sup \; s^{-1} \ f = \sup_{x \in s} f(x^{-1}) $$$

Lean4

@[to_additive (attr := simp)]
theorem sup_inv [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : sup s⁻¹ f = sup s (f ·⁻¹) :=
  sup_image ..

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