mem_closure_singleton — Mathlib

English

If e is nonloop and e ∈ closure of {f}, then f ∈ closure of {e}.

Русский

Если e не петля и e ∈ closure({f}), тогда f ∈ closure({e}).

LaTeX

$$$ M.IsNonloop e \rightarrow e \in M.closure \{ f \} \rightarrow f \in M.closure \{ e \} $$$

Lean4

theorem mem_closure_singleton (he : M.IsNonloop e) (hef : e ∈ M.closure { f }) : f ∈ M.closure { e } :=
  by
  rw [← union_empty {_}, singleton_union] at *
  exact (M.closure_exchange (X := ∅) ⟨hef, (isNonloop_iff_notMem_loops he.mem_ground).1 he⟩).1

Похожие утверждения