inf'_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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