English
The strong elimination axiom: for any distinct circuits C1, C2 and e ∈ C1 ∩ C2 and f ∈ C1 \\ C2 with f not in C2, there exists a circuit C contained in (C1 ∪ C2) \\ {e} that contains f.
Русский
Аксиома сильного устранения: для любых различных окружностей C1, C2 и e ∈ C1 ∩ C2, f ∈ C1 \ C2 и f ∉ C2 существует окружность C ⊆ (C1 ∪ C2) \\ {e}, такая что f ∈ C.
LaTeX
$$$\\forall {\\alpha} {M : Matroid α} {C_1 C_2 : Set α}, M.IsCircuit C_1 \\to M.IsCircuit C_2 \\to e \\in C_1 \\to e \\in C_2 \\to f \\in C_1 \\to f \\notin C_2 \\to ∃ C \\subseteq (C_1 \\cup C_2) \\setminus { e }, M.IsCircuit C ∧ f ∈ C$$$
Lean4
/-- The strong isCircuit elimination axiom. For any pair of distinct circuits `C₁, C₂` and all
`e ∈ C₁ ∩ C₂` and `f ∈ C₁ \ C₂`, there is a circuit `C` with `f ∈ C ⊆ (C₁ ∪ C₂) \ {e}`. -/
theorem strong_elimination (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (heC₁ : e ∈ C₁) (heC₂ : e ∈ C₂) (hfC₁ : f ∈ C₁)
(hfC₂ : f ∉ C₂) : ∃ C ⊆ (C₁ ∪ C₂) \ { e }, M.IsCircuit C ∧ f ∈ C :=
by
obtain ⟨C, hCs, hC, hfC⟩ :=
hC₁.strong_multi_elimination (fun i : Unit ↦ e) (fun _ ↦ C₂) f (by simpa) (by simpa) (by simpa) (by simp) (by simpa)
(by simpa)
exact ⟨C, hCs.trans (diff_subset_diff (by simp) (by simp)), hC, hfC⟩
