English
For an embedding f : γ ↪ β, and hs stating the nonempty of the mapped Finset, the infimum over the mapped set with g equals the infimum over s of g ∘ f; i.e., inf' over map f equals inf' with precomposition.
Русский
Для вложения f: γ → β и непустости образа, инфимуум над образованием через map f равен инфимумума над исходным множеством с предобразованием.
LaTeX
$$$(\\mathrm{map}\\ f\\ s).inf' hs g = s.inf' (map_nonempty.1 hs) (g \\circ f)$$$
Lean4
/-- To rewrite from right to left, use `Finset.inf'_comp_eq_map`. -/
@[simp]
theorem inf'_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f).Nonempty) :
(s.map f).inf' hs g = s.inf' (map_nonempty.1 hs) (g ∘ f) :=
sup'_map (α := αᵒᵈ) _ hs
