disjSum_inj — Mathlib

English

Let s1, s2 be finite subsets of α and t1, t2 be finite subsets of β. Then s1 ⊎ t1 = s2 ⊎ t2 if and only if s1 = s2 and t1 = t2.

Русский

Пусть s1, s2 — конечные подмножества α, а 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

@[simp]
theorem disjSum_inj {α β : Type*} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} :
    s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂ := by simp [Finset.ext_iff]

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