Injective2_disjSum — Mathlib

English

The disjoint sum operation is jointly injective in its two arguments: if s1 ⊎ t1 = s2 ⊎ t2, then s1 = s2 and t1 = t2.

Русский

Операция дизъюнктивного суммирования инъективна по обоим аргументам: если s1 ⊎ t1 = s2 ⊎ t2, то s1 = s2 и t1 = t2.

LaTeX

$$$ s_1 \uplus t_1 = s_2 \uplus t_2 \iff s_1 = s_2 \land t_1 = t_2 $$$

Lean4

theorem Injective2_disjSum {α β : Type*} : Function.Injective2 (@disjSum α β) := fun _ _ _ _ => by simp [Finset.ext_iff]

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