English
Let α be a semilattice with infimum. Let s be a nonempty finite subset of γ, let f: γ ↪ β be an embedding, and let g: β → α. Then the infimum of g ∘ f over s equals the infimum of g over the image of s.
Русский
Пусть α — полулинейная частично упорядоченная структура с операцией meet. Пусть s — непустое конечное подмножество γ, f: γ ↪ β — вложение, и g: β → α. Тогда infimum of g ∘ f над s равен infimum of g над образцом s.
LaTeX
$$$s \neq \varnothing \;\Rightarrow\; \inf_{x \in s} g(f(x)) = \inf_{y \in f(s)} g(y)$$$
Lean4
/-- A version of `Finset.inf'_map` 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_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) :
s.inf' hs (g ∘ f) = (s.map f).inf' (map_nonempty.2 hs) g :=
sup'_comp_eq_map (α := αᵒᵈ) g hs
