fundCircuit_diff_eq_inter — Mathlib

English

If e ∉ I, then (fundCircuit e I) \ {e} = (fundCircuit e I) ∩ I.

Русский

Если e ∉ I, то (fundCircuit e I) \ {e} = (fundCircuit e I) ∩ I.

LaTeX

$$$(M.fundCircuit\ e\ I)\setminus\{e\} = (M.fundCircuit\ e\ I)\cap I$$$

Lean4

theorem fundCircuit_diff_eq_inter (M : Matroid α) (heI : e ∉ I) :
    (M.fundCircuit e I) \ { e } = (M.fundCircuit e I) ∩ I :=
  (subset_inter diff_subset (by simp [fundCircuit_subset_insert])).antisymm
    (subset_diff_singleton inter_subset_left (by simp [heI]))

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