English
The closure-exchange relation is symmetric: e belongs to closure of insert f X minus closure X if and only if f belongs to closure of insert e X minus closure X.
Русский
Обмен замыканием симметричен: e ∈ cl(insert f X) \\ cl(X) эквивалентно f ∈ cl(insert e X) \\ cl(X).
LaTeX
$$$ e \\in M.\\mathrm{closure}(\\mathrm{insert}(f,X)) \\setminus M.\\mathrm{closure}(X) \\; \\Leftrightarrow\\; f \\in M.\\mathrm{closure}(\\mathrm{insert}(e,X)) \\setminus M.\\mathrm{closure}(X) $$$
Lean4
theorem closure_exchange (he : e ∈ M.closure (insert f X) \ M.closure X) : f ∈ M.closure (insert e X) \ M.closure X :=
⟨mem_closure_insert he.2 he.1, fun hf ↦ by
rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (notMem_empty _)] at he⟩
