inf_inv — Mathlib

English

For Finset s and function f, the infimum of s⁻¹ with respect to f equals the infimum of s with respect to f composed with inversion: inf s⁻¹ f = inf s (f ·⁻¹).

Русский

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

LaTeX

$$$ \inf \; s^{-1} \; f = \inf_{x \in s} f(x^{-1}) $$$

Lean4

@[to_additive (attr := simp)]
theorem inf_inv [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) : inf s⁻¹ f = inf s (f ·⁻¹) :=
  inf_image ..

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