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 indep_iff_forall_closure_diff_ne : M.Indep I ↔ ∀ ⦃e⦄, e ∈ I → M.closure (I \ { e }) ≠ M.closure I :=
by
rw [indep_iff_forall_notMem_closure_diff']
refine
⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)), fun h ↦
⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_, fun e heI hin ↦ h heI ?_⟩⟩
·
rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left, inter_singleton_eq_empty.mpr heE, diff_empty,
inter_comm, closure_inter_ground]
nth_rw 2 [show I = insert e (I \ { e }) by simp [heI]]
rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]
