eq_union_image_of_disjointSum — Mathlib

English

If the disjointSum is a base for B, then B can be written as a union of two independent parts from the two components.

Русский

Если disjointSum имеет базис B, то B можно представить как объединение двух независимых частей из двух компонентов.

LaTeX

$$$$ \exists BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN. $$$$

Lean4

theorem eq_union_image_of_disjointSum {h B} (hB : (disjointSum M N h).IsBase B) :
    ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN :=
  by
  rw [disjointSum_isBase_iff] at hB
  refine ⟨_, _, hB.1, hB.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩
  rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hB.2.2]

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