isClosedMap_sumElim — Mathlib

English

A simplified equivalence: IsClosedMap( Sum.elim f g ) iff IsClosedMap f ∧ IsClosedMap g.

Русский

Упрощённая эквивалентность: IsClosedMap( Sum.elim f g ) эквивалентно IsClosedMap f ∧ IsClosedMap g.

LaTeX

$$$$\\mathrm{IsClosedMap}(\\mathrm{Sum.elim} f g) \\iff \\mathrm{IsClosedMap} f \\land \\mathrm{IsClosedMap} g.$$$$

Lean4

@[simp]
theorem isClosedMap_sumElim {f : X → Z} {g : Y → Z} : IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g := by
  simp only [isClosedMap_sum, Sum.elim_inl, Sum.elim_inr]

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