eRk_le_iff — Mathlib

English

eRk X = 0 iff X ∩ E ⊆ loops (i.e., X contains only loops from the ground).

Русский

eRk(X) = 0 тогда и только тогда X ∩ E ⊆ петли (то есть X содержит только петли из опорного множества).

LaTeX

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

Lean4

theorem eRk_le_iff : M.eRk X ≤ n ↔ ∀ ⦃I⦄, I ⊆ X → M.Indep I → I.encard ≤ n :=
  by
  refine ⟨fun h I hIX hI ↦ (hI.eRk_eq_encard.symm.trans_le ((M.eRk_mono hIX).trans h)), fun h ↦ ?_⟩
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.encard_eq_eRk]
  exact h hI.subset hI.indep

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