English
If e lies in the exchange region for insert f X, then replacing f by e in the insert yields the same closure as replacing e by f.
Русский
Если e принадлежит области обмена при вставке f X, то замыкания after вставки e совпадают с замыканием после вставки f.
LaTeX
$$$ \\forall h,\\; M.\\mathrm{closure}(\\mathrm{insert}(f,X)) \\setminus M.\\mathrm{closure}(X) \\ni e \\Rightarrow M.\\mathrm{closure}(\\mathrm{insert}(e,X)) = M.\\mathrm{closure}(\\mathrm{insert}(f,X)) $$$
Lean4
theorem closure_insert_congr (he : e ∈ M.closure (insert f X) \ M.closure X) :
M.closure (insert e X) = M.closure (insert f X) :=
by
have hf := closure_exchange he
rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert, insert_comm, ←
closure_closure, ← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hf.1, closure_closure,
closure_closure]
