English
M.Indep I is equivalent to ∀ e ∈ I, closure(I\{e}) ≠ closure(I).
Русский
Эквивалентно: M.Indep I эквивалентно ∀ e ∈ I, closure(I\{e}) ≠ closure(I).
LaTeX
$$$M.Indep I \iff \forall e \in I,\ M.closure(I\setminus\{e\}) \neq M.closure I$$$
Lean4
theorem union_indep_iff_forall_notMem_closure_right (hI : M.Indep I) (hJ : M.Indep J) :
M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ (J \ { e })) :=
by
refine ⟨fun h e heJ hecl ↦ h.notMem_closure_diff_of_mem (.inr heJ.1) ?_, fun h ↦ ?_⟩
· rwa [union_diff_distrib, diff_singleton_eq_self heJ.2]
obtain ⟨K, hKIJ, hK⟩ := hI.subset_isBasis_of_subset (show I ⊆ I ∪ J from subset_union_left)
obtain rfl | hssu := hKIJ.subset.eq_or_ssubset
· exact hKIJ.indep
exfalso
obtain ⟨e, heI, heK⟩ := exists_of_ssubset hssu
have heJI : e ∈ J \ I := by
rw [← union_diff_right, union_comm]
exact ⟨heI, notMem_subset hK heK⟩
refine h _ heJI ?_
rw [← diff_singleton_eq_self heJI.2, ← union_diff_distrib]
exact M.closure_subset_closure (subset_diff_singleton hKIJ.subset heK) <| hKIJ.subset_closure heI
