inf'_comp_eq_image — Mathlib

English

If g preserves infimum, then applying g to the infimum over s yields the same as taking the infimum over the composed map; i.e., g(s.inf' H f) = s.inf' H (g ∘ f).

Русский

Если функция g сохраняет инфимума, то применение g к инфимума над s равно инфимумума над композиции g ∘ f.

LaTeX

$$$g( s.inf' H f ) = s.inf' H (g \\circ f)$$$

Lean4

/-- A version of `Finset.inf'_image` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty. -/
theorem inf'_comp_eq_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : s.Nonempty) (g : β → α) :
    s.inf' hs (g ∘ f) = (s.image f).inf' (hs.image f) g :=
  sup'_comp_eq_image (α := αᵒᵈ) hs g

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