mem_closure_comm — Mathlib

English

If e and f are nonloops, then f ∈ closure {e} iff e ∈ closure {f}.

Русский

Если e и f — не петли, то f ∈ closure({e}) эквивалентно e ∈ closure({f}).

LaTeX

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

Lean4

theorem mem_closure_comm (he : M.IsNonloop e) (hf : M.IsNonloop f) : f ∈ M.closure { e } ↔ e ∈ M.closure { f } :=
  ⟨hf.mem_closure_singleton, he.mem_closure_singleton⟩

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