eRk_eq_zero_iff' — Mathlib

English

eRk X = 0 iff X ∩ E ⊆ loops

Русский

eRk X = 0 тогда и только тогда X ∩ E ⊆ петли

LaTeX

$$$ M.eRk X = 0 \\iff X \\cap M.E \\subseteq M.loops $$$

Lean4

/-- A version of `erk_eq_zero_iff'` with no supportedness hypothesis. -/
theorem eRk_eq_zero_iff' : M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
  rw [← eRk_inter_ground, ← hI.encard_eq_eRk, encard_eq_zero]
  refine ⟨fun h ↦ by simpa [h] using hI, fun h ↦ eq_empty_iff_forall_notMem.2 fun e heI ↦ ?_⟩
  exact (hI.indep.isNonloop_of_mem heI).not_isLoop (h (hI.subset heI))

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