eq_union_image_of_disjointSum — Mathlib

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]

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