sup_map — Mathlib

English

If f is an embedding, then the supremum of the mapped set equals the mapped supremum composition: (s.map f).sup g = s.sup (g ∘ f).

Русский

Если f — вложение, то верхняя грань отображённого множества равна верхней грани композиции: (s.map f).sup g = s.sup (g ∘ f).

LaTeX

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

Lean4

@[simp]
theorem sup_map (s : Finset γ) (f : γ ↪ β) (g : β → α) : (s.map f).sup g = s.sup (g ∘ f) :=
  fold_map

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