eq_freeOn_iff — Mathlib

English

For a matroid M on α and a subset E of α, M equals freeOn E if and only if the ground M.E equals E and E is independent in M.

Русский

Пусть матроид M на α и подмножество E. Тогда M = freeOn(E) тогда и только тогда, когда M.E = E и E независимо в M.

LaTeX

$$$ M = freeOn E \iff M.E = E \land M.Indep E $$$

Lean4

theorem eq_freeOn_iff : M = freeOn E ↔ M.E = E ∧ M.Indep E :=
  by
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro rfl; simp
  simp only [ext_iff_indep, freeOn_ground, freeOn_indep_iff, h.1, true_and]
  exact fun I hIX ↦ iff_of_true (h.2.subset hIX) hIX

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