English
If e is not in closure X but e lies in the closure of X with a new element f, then f lies in the closure of X with e added.
Русский
Если e не принадлежит closure(X), но содержится в closure(X ∪ {f}), то f принадлежит closure(X ∪ {e}).
LaTeX
$$$ \\text{If } e \\notin M.\\mathrm{closure}(X) \\text{ and } e \\in M.\\mathrm{closure}(\\mathrm{insert}(f,X)), \\; f \\in M.\\mathrm{closure}(\\mathrm{insert}(e,X)) $$$
Lean4
theorem mem_closure_insert (he : e ∉ M.closure X) (hef : e ∈ M.closure (insert f X)) : f ∈ M.closure (insert e X) :=
by
rw [← closure_inter_ground] at *
have hfE : f ∈ M.E := by by_contra! hfE; rw [insert_inter_of_notMem hfE] at hef; exact he hef
have heE : e ∈ M.E := (M.closure_subset_ground _) hef
rw [insert_inter_of_mem hfE] at hef; rw [insert_inter_of_mem heE]
obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
rw [← hI.closure_eq_closure, hI.indep.notMem_closure_iff] at he
rw [← closure_insert_closure_eq_closure_insert, ← hI.closure_eq_closure, closure_insert_closure_eq_closure_insert,
he.1.mem_closure_iff] at *
rw [or_iff_not_imp_left, dep_iff, insert_comm,
and_iff_left (insert_subset heE (insert_subset hfE hI.indep.subset_ground)), not_not]
intro h
rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff, or_iff_left he.2] at hef
subst hef; apply mem_insert
