English
Infinite strong circuit elimination: given a circuit C0, a family of circuits Ci, elements x_i in Ci, and z in C0 but outside all Ci, there exists a circuit C' contained in the union that still contains z and avoids all x_i.
Русский
Бесконечная сильная индукция окружностей: дано C0 и семейство окружностей Ci; элементы x_i в Ci и z в C0, но вне всех Ci; существует окружность C', содержащая z и не содержащая ни одного x_i, внутри объединения.
LaTeX
$$$\\forall {\\alpha} {M : Matroid \\alpha} {\\iota : Type*} {C_0 : Set α},\\ M.IsCircuit C_0 \\to \\forall (x : \\iota → α) (C : \\iota → Set α) (z : α),\\ (\\forall i, M.IsCircuit (C i)) \\to (\\forall i, x i ∈ C_0) \\to (\\forall i, x i ∈ C i) \\to (\\forall ⦃i i'⦄, x i ∈ C i' → i = i') \\to z ∈ C_0 \\to (\\forall i, z ∉ C i) \\to ∃ C' ⊆ (C_0 ∪ ⋃ i, C i) \\setminus range x, M.IsCircuit C' ∧ z ∈ C'$$$
Lean4
/-- A generalization of the strong circuit elimination axiom `Matroid.IsCircuit.strong_elimination`
to an infinite collection of circuits.
It states that, given a circuit `C₀`, a arbitrary collection `C : ι → Set α` of circuits,
an element `x i` of `C₀ ∩ C i` for each `i`, and an element `z ∈ C₀` outside all the `C i`,
the union of `C₀` and the `C i` contains a circuit containing `z` but none of the `x i`.
This is one of the axioms when defining infinite matroids via circuits.
TODO : A similar statement will hold even when all mentions of `z` are removed. -/
theorem strong_multi_elimination (hC₀ : M.IsCircuit C₀) (x : ι → α) (C : ι → Set α) (z : α)
(hC : ∀ i, M.IsCircuit (C i)) (h_mem_C₀ : ∀ i, x i ∈ C₀) (h_mem : ∀ i, x i ∈ C i)
(h_unique : ∀ ⦃i i'⦄, x i ∈ C i' → i = i') (hzC₀ : z ∈ C₀) (hzC : ∀ i, z ∉ C i) :
∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C' :=
by
have hwin :=
IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i})) (J := C₀ \ range x) (z := z) (by simp)
(fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
· obtain ⟨C', hC'ss, hC', hzC'⟩ := hwin
refine ⟨C', hC'ss.trans ?_, hC', hzC'⟩
refine
union_subset (diff_subset_diff_left subset_union_left)
(iUnion_subset fun i ↦
subset_diff.2 ⟨diff_subset.trans (subset_union_of_subset_right (subset_iUnion ..) _), ?_⟩)
rw [disjoint_iff_forall_ne]
rintro _ he _ ⟨j, hj, rfl⟩ rfl
obtain rfl : j = i := h_unique he.1
simp at he
· simpa [insert_eq_of_mem (h_mem i)] using hC i
· rwa [diff_union_self, union_eq_self_of_subset_right]
rintro _ ⟨i, hi, rfl⟩
exact h_mem_C₀ i
· rintro ⟨i, hi, rfl⟩
exact hzC _ (h_mem i)
simp only [mem_diff, mem_singleton_iff, not_and, not_not]
exact fun i hzi ↦ (hzC i hzi).elim
