sup_image — Mathlib

English

The supremum of the image of s under f equals the supremum of f∘f over s; in particular, (s.image f).sup g = s.sup (g ∘ f).

Русский

Наибольшая грань образа s через f равна наибольшей грани композиции g с f над s.

LaTeX

$$$ (s.image f).sup g = s.sup (g \\circ f) $$$

Lean4

@[simp]
theorem sup_image [DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α) : (s.image f).sup g = s.sup (g ∘ f) :=
  fold_image_idem

Похожие утверждения