augment_finset — Mathlib

English

For finite independent sets I, J of a matroid M, if |I| < |J|, there exists an element e ∈ J \ I such that I ∪ {e} is independent.

Русский

Для двух конечных независимых множеств I, J в матроида M, если |I| < |J|, существует элемент e ∈ J \ I такой, что I ∪ {e} независимо.

LaTeX

$$$\\exists e \\in J, e \\notin I \\land M.Indep(I \\cup \\{e\\})$$$

Lean4

theorem augment_finset {I J : Finset α} (hI : M.Indep I) (hJ : M.Indep J) (hIJ : I.card < J.card) :
    ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e I) :=
  by
  obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card])
  simp only [mem_diff, Finset.mem_coe] at hx
  exact ⟨x, hx.1, hx.2, hxI⟩

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