English
A variant where the collection of circuits is a Set S of circuits and the distinguished elements are a Set X; under hypotheses there exists a circuit C' contained in (C0 ∪ S.sUnion) \\ X containing z.
Русский
Вариант, где коллекция окружностей — множество S, а выделенные элементы — множество X; при гипотезах существует C' ⊆ (C0 ∪ S.sUnion) \\ X, содержащая z.
LaTeX
$$$\\forall {\\alpha} {M : Matroid α} {C_0} (hC_0 : M.IsCircuit C_0) (X : Set α) (S : Set (Set α)) (z : α), (\\forall C ∈ S, M.IsCircuit C) \\to X ⊆ C_0 \\to (\\forall x, x \\in X \\to \\exists C ∈ S, C ∩ X = { x }) \\to z \\in C_0 \\to (\\forall C ∈ S, z \\notin C) \\to ∃ C' ⊆ (C_0 ∪ S.sUnion) \\setminus X, M.IsCircuit C' ∧ z ∈ C'$$$
Lean4
/-- The circuit elimination axiom : for any pair of distinct circuits `C₁, C₂` and any `e`,
some circuit is contained in `(C₁ ∪ C₂) \ {e}`.
This is one of the axioms when defining a finitary matroid via circuits;
as an axiom, it is usually stated with the extra assumption that `e ∈ C₁ ∩ C₂`. -/
theorem elimination (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (h : C₁ ≠ C₂) (e : α) :
∃ C ⊆ (C₁ ∪ C₂) \ { e }, M.IsCircuit C :=
by
have hnss : ¬(C₁ ⊆ C₂) := fun hss ↦ h <| hC₁.eq_of_subset_isCircuit hC₂ hss
obtain ⟨f, hf₁, hf₂⟩ := not_subset.1 hnss
by_cases he₁ : e ∈ C₁
· by_cases he₂ : e ∈ C₂
· obtain ⟨C, hC, hC', -⟩ := hC₁.strong_elimination hC₂ he₁ he₂ hf₁ hf₂
exact ⟨C, hC, hC'⟩
exact ⟨C₂, subset_diff_singleton subset_union_right he₂, hC₂⟩
exact ⟨C₁, subset_diff_singleton subset_union_left he₁, hC₁⟩
