indep_singleton — Mathlib

English

Not a nonloop e is equivalent to closure of {e} equals the loops set (simplified).

Русский

Не-не-петля e эквивалентна тому, что замыкание {e} равно петлям (упрощено).

LaTeX

$$$ \neg M.IsNonloop e \iff M.closure \{ e \} = M.loops $$$

Lean4

@[simp]
theorem indep_singleton : M.Indep { e } ↔ M.IsNonloop e :=
  by
  rw [isNonloop_iff, ← singleton_dep, dep_iff, not_and, not_imp_not, singleton_subset_iff]
  exact ⟨fun h ↦ ⟨fun _ ↦ h, singleton_subset_iff.mp h.subset_ground⟩, fun h ↦ h.1 h.2⟩

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