English
A function between types yields a sup-preserving map between their lattices of subsets by taking images.
Русский
Функция между типами порождает суп-однородный гомоморфизм между решётками подмножеств посредством образов.
LaTeX
$$$$ \mathrm{setImage}(f) : \mathrm{sSupHom}(\mathrm{Set}\,\alpha, \mathrm{Set}\,\beta) \quad \text{with} \quad \mathrm{toFun}(\mathrm{setImage}(f)) = \mathrm{image}(f), \ \mathrm{map\_sSup}'(\mathrm{setImage}(f)) = \mathrm{Set.image\_sSup}. $$$$
Lean4
/-- Using `Set.image`, a function between types yields a `sSupHom` between their lattices of
subsets.
See also `CompleteLatticeHom.setPreimage`. -/
@[simps]
def setImage (f : α → β) : sSupHom (Set α) (Set β)
where
toFun := image f
map_sSup' := Set.image_sSup
