inf'_image — Mathlib

English

The infimum over the image of s under f equals the infimum over s of the composed function, provided both sides are defined; this equates the two presentations of infimum via image.

Русский

Инфиму об изображении множества через f равен инфимууму над исходным множеством для составной функции.

LaTeX

$$$(\\mathrm{image}\; f\\; s).inf' hs g = s.inf' hs.of_image (g \\circ f)$$$

Lean4

/-- To rewrite from right to left, use `Finset.inf'_comp_eq_image`. -/
@[simp]
theorem inf'_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (s.image f).Nonempty) (g : β → α) :
    (s.image f).inf' hs g = s.inf' hs.of_image (g ∘ f) :=
  @sup'_image αᵒᵈ _ _ _ _ _ _ hs _

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