fundCircuit_restrict — Mathlib

English

The fundCircuit of e with respect to I is unchanged under restriction to a subset R containing I and e, provided R is contained in the ground E.

Русский

Фундконтур e относительно I не изменяется при ограничении матроида до множества R, если I ⊆ R, e ∈ R и R ⊆ E.

LaTeX

$$$\\forall {I R : Set \\alpha} (M : Matroid \\alpha) (e : \\alpha), I \\subseteq R \\to e \\in R \\to R \\subseteq M.E \\to (M \\downarrow R).fundCircuit e I = M.fundCircuit e I$$$

Lean4

theorem fundCircuit_restrict {R : Set α} (hIR : I ⊆ R) (heR : e ∈ R) (hR : R ⊆ M.E) :
    (M ↾ R).fundCircuit e I = M.fundCircuit e I :=
  by
  simp_rw [fundCircuit, M.restrict_closure_eq (R := R) (X := { e }) (by simpa)]
  apply subset_antisymm
  · gcongr 5 with J hJI; intro heJ
    simp only [restrict_closure_eq']
    refine (inter_subset_inter_left _ ?_).trans subset_union_left
    rwa [inter_eq_self_of_subset_left (hJI.trans hIR)]
  gcongr 5 with J hJI; intro heJ
  refine closure_subset_closure_of_subset_closure ?_
  rw [restrict_closure_eq _ (hJI.trans hIR) hR] at heJ
  simp only [subset_inter_iff, inter_subset_right, and_true] at heJ
  exact subset_trans (by simpa [M.mem_closure_of_mem' (mem_singleton e) (hR heR)]) heJ

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