fundCircuit_restrict_univ — Mathlib

English

The fundCircuit is preserved under restriction to the whole universe: (M| univ).fundCircuit e I = M.fundCircuit e I.

Русский

Фундконтур сохраняется при ограничении до всего вселенной: (M|univ).fundCircuit e I = M.fundCircuit e I.

LaTeX

$$$(M|_{\\mathrm{univ}}).fundCircuit e I = M.fundCircuit e I$$$

Lean4

@[simp]
theorem fundCircuit_restrict_univ (M : Matroid α) : (M ↾ univ).fundCircuit e I = M.fundCircuit e I :=
  by
  have aux (A B) : M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B :=
    by
    refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
    refine (subset_inter h (M.closure_subset_ground A)).trans ?_
    simp [union_inter_distrib_right]
  simp [fundCircuit, aux]

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