disjSum — Mathlib

English

If s and t are noduplicates, then s.disjSum t is also nodup.

Русский

Если s и t не имеют повторов, то s.disjSum t тоже без повторов.

LaTeX

$$$ (s.Nodup) \\land (t.Nodup) \\Rightarrow (s.disjSum t).Nodup $$$

Lean4

protected theorem disjSum (hs : s.Nodup) (ht : t.Nodup) : (s.disjSum t).Nodup :=
  by
  refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_
  rw [disjoint_map_map]
  exact fun _ _ _ _ ↦ inr_ne_inl.symm

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