image_sSup — Mathlib

English

The image of the supremum (union) of a family of sets under f equals the supremum of the images.

Русский

Образ верхнего предела (объединение) семейства множеств под действием f равен верхнему пределу образов.

LaTeX

$$$$ f'' \mathrm{sSup} s = \mathrm{sSup} (\mathrm{image}\, f''\, s). $$$$

Lean4

theorem image_sSup {f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (image f '' s) :=
  Set.image_sUnion

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