union_indep_iff_forall_notMem_closure_left

English

If I and J are independent, then I ∪ J is independent iff ∀ e ∈ J \ I, e ∉ closure(I ∪ (J \ {e})).

Русский

Если I и J независимы, то I ∪ J независим тогда и только тогда, когда ∀ e ∈ J \ I, e ∉ closure(I ∪ (J \ {e})).

LaTeX

$$$M.Indep I \rightarrow M.Indep J \rightarrow M.Indep(I \cup J) \iff \forall e \in J \setminus I, e \notin M.closure(I \cup (J \setminus \{e\}))$$$

Lean4

theorem union_indep_iff_forall_notMem_closure_left (hI : M.Indep I) (hJ : M.Indep J) :
    M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure ((I \ { e }) ∪ J) := by
  simp_rw [union_comm I J, hJ.union_indep_iff_forall_notMem_closure_right hI, union_comm]

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