sumMap — Mathlib

English

Let f: α → γ and g: β → δ be bijections. Then Sum.map f g is a bijection α ⊕ β → γ ⊕ δ.

Русский

Пусть f: α → γ и g: β → δ — биекции. Тогда Sum.map f g — биекция α ⊕ β → γ ⊕ δ.

LaTeX

$$(\operatorname{Bijective} f) ∧ (\operatorname{Bijective} g) ⇒ \operatorname{Bijective}(\mathrm{Sum.map}\, f\, g).$$

Lean4

theorem sumMap {f : α → β} {g : α' → β'} (hf : Bijective f) (hg : Bijective g) : Bijective (Sum.map f g) :=
  ⟨hf.injective.sumMap hg.injective, hf.surjective.sumMap hg.surjective⟩

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