English
For Finset γ, an embedding f : γ ↪ β and a map g : β → α with Nonempty Finset map s, the supremum over the mapped finset equals the supremum over the original finset composed with f.
Русский
Для Finset γ и вложения f: γ ↪ β и отображения g: β → α, выполнено равенство sup' над image и над исходным с учётом композиции.
LaTeX
$$$ (Finset.map f s).sup' hs g = s.sup' ⋯ (g \circ f)$$$
Lean4
/-- To rewrite from right to left, use `Finset.sup'_comp_eq_map`. -/
@[simp]
theorem sup'_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f).Nonempty) :
(s.map f).sup' hs g = s.sup' (map_nonempty.1 hs) (g ∘ f) :=
by
rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']
rfl
