English
If a subset I is independent in the disjointSum, then it can be partitioned into two independent parts I_M and I_N on the two components such that I = I_M ∪ I_N and I_M ∩ I_N = ∅.
Русский
Если подмножество I независимо в disjointSum, то его можно разложить на две независимые части I_M и I_N на двух компонентах так, чтобы I = I_M ∪ I_N и I_M ∩ I_N = ∅.
LaTeX
$$$$ \exists IM IN, M.Indep IM \land N.Indep IN \land Disjoint IM IN \land I = IM \cup IN. $$$$
Lean4
theorem eq_union_image_of_disjointSum {h I} (hI : (disjointSum M N h).Indep I) :
∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN :=
by
rw [disjointSum_indep_iff] at hI
refine ⟨_, _, hI.1, hI.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]