isNonloop_of_mem_closure — Mathlib

English

Let M be a matroid and let e, f be elements. If e is a nonloop and e lies in the closure of {f}, then f is a nonloop.

Русский

Пусть M — матроид и e, f — элементы. Если e не петля и e принадлежит замыканию множества {f}, то f тоже не петля.

LaTeX

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

Lean4

theorem isNonloop_of_mem_closure (he : M.IsNonloop e) (hef : e ∈ M.closure { f }) : M.IsNonloop f :=
  by
  rw [isNonloop_iff, and_comm]
  by_contra! h; apply he.not_isLoop
  rw [isLoop_iff] at *; convert hef using 1
  obtain (hf | hf) := em (f ∈ M.E)
  · rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops, insert_empty_eq]
  rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]

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