pushforward_union — Mathlib

English

For any f: Y → X and sieve S and R on Y, the pushforward under f distributes over the union: pushforward f (S ⊔ R) = pushforward f S ⊔ pushforward f R.

Русский

Для любого стрелы f: Y → X и сита S,R на Y перенос через f дистрибутивен над суммой: pushforward f (S ⊔ R) = pushforward f S ⊔ pushforward f R.

LaTeX

$$$\mathrm{pushforward}\, f\bigl(S\sqcup R\bigr) = \mathrm{pushforward}\, f\,S \sqcup \mathrm{pushforward}\, f\,R$$$

Lean4

theorem pushforward_union {f : Y ⟶ X} (S R : Sieve Y) : (S ⊔ R).pushforward f = S.pushforward f ⊔ R.pushforward f :=
  (galoisConnection f).l_sup

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