Skip to content
Axiomatic Wiki
Lemma·L61

Basic properties of the disjoint union

The two tagging maps are injective, and their images are disjoint and cover the whole disjoint union.

Let be sets, with and from D076. Then: (i) and are injective; (ii) ; (iii) .
In words
inl embeds A and inr embeds B into the disjoint union: inl and inr are injective, their images meet in nothing, and their images union to all of A⊔B.
Rests onF02F03F04F06F08F09F14A01A02A08
Never needed: F05 · F10 · F11 · F12 · F13 · A03 · A04 · A05 · A06 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    (i) If , i.e. , then by the characteristic property of ordered pairs. Symmetrically, gives .
  2. 2
    (ii) Suppose (D008). Then for some and for some (D007). By L01, forces . But (D026), so would give , contradicting (P3) at ( ). So no such exists: (D002).
  3. 3
    (iii) By D007, , and likewise . By D076, .
∎

Remarks

Justifies calling a genuine "side by side" combination of and : every element of the disjoint union comes from exactly one side, unambiguously, and every element of or has exactly one corresponding element inside. Together, (ii) and (iii) say is a partition of into (at most) two pieces.
Wikipedia ↗Sum.inl_injective ↗
Propose an edit1 published revision