English
Let α be a semilattice with join, and γ, β be types. For a finite nonempty set s of γ, an embedding f : γ → β, and a function g : β → α, we have that the supremum of g ∘ f over s equals the supremum of g over the image of s under f; i.e. sup_{x∈s} g(f(x)) = sup_{y∈f(s)} g(y).
Русский
Пусть α — полукольцо с операцией объединения (верхняя граница), а γ, β — множества. Для конечного непустого множества s ⊆ γ, вложения f: γ → β и функции g: β → α имеет место равенство: sup_{x∈s} g(f(x)) = sup_{y∈f(s)} g(y).
LaTeX
$$$\\displaystyle \\sup_{x \\in s} g(f(x)) = \\sup_{y \\in f[s]} g(y)$$$
Lean4
/-- A version of `Finset.sup'_map` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty. -/
theorem sup'_comp_eq_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) :
s.sup' hs (g ∘ f) = (s.map f).sup' (map_nonempty.2 hs) g :=
.symm <| sup'_map _ _
