English
A map on a sum is closed iff its restrictions to each summand are closed maps.
Русский
Отображение на сумме замкнуто тогда, когда его ограничения на каждую компоненту замкнуты.
LaTeX
$$$$\\mathrm{IsClosedMap}(f) \\iff \\Big(\\mathrm{IsClosedMap}(\\lambda a. f(\\mathrm{Sum.inl} a))\\Big) \\land \\mathrm{IsClosedMap}(\\lambda b. f(\\mathrm{Sum.inr} b)).$$$$
Lean4
theorem isClosedMap_sum {f : X ⊕ Y → Z} :
IsClosedMap f ↔ (IsClosedMap fun a => f (.inl a)) ∧ IsClosedMap fun b => f (.inr b) :=
by
constructor
· intro h
exact ⟨h.comp IsClosedEmbedding.inl.isClosedMap, h.comp IsClosedEmbedding.inr.isClosedMap⟩
· rintro h Z hZ
rw [isClosed_sum_iff] at hZ
convert (h.1 _ hZ.1).union (h.2 _ hZ.2)
ext
simp only [mem_image, Sum.exists, mem_union, mem_preimage]
