English
If e is an order isomorphism between α and β, then applying e to the truncatedSup over s at a equals the truncatedSup over the image of s at e(a).
Русский
Пусть e — биекция упорядочения между α и β. Тогда отображение e сохраняет усечённый верхний предел: e(truncatedSup s a) = truncatedSup (map s) (e a).
LaTeX
$$$e\bigl(\operatorname{truncatedSup} s \, a\bigr) = \operatorname{truncatedSup}\bigl((s.{map} e.toEquiv.toEmbedding)\bigr)\,(e a)$$
Lean4
theorem map_truncatedSup [DecidableLE β] (e : α ≃o β) (s : Finset α) (a : α) :
e (truncatedSup s a) = truncatedSup (s.map e.toEquiv.toEmbedding) (e a) :=
by
have : e a ∈ lowerClosure (s.map e.toEquiv.toEmbedding : Set β) ↔ a ∈ lowerClosure s := by simp
simp_rw [truncatedSup, apply_dite e, map_finset_sup', map_top, this]
congr with h
simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv, OrderIso.le_iff_le, id,
sup'_map]
