English
An insertion-based version of the strong multi-elimination axiom: given a family of circuits indexed by i, there is a circuit containing z but avoiding all x_i.
Русский
Версия аксиомы сильной многоэллиминации через вставку: дана семейство окружностей, индексируемых i, существует окружность, содержащая z, но не содержащая все x_i.
LaTeX
$$$\\forall {\\alpha} {M : Matroid \\alpha} {\\iota : Type*} {J : Set α} (x : \\iota → α) (I : \\iota → Set α) (z : α),\\ (\\forall i, M.IsCircuit (insert (x i) (I i))) \\to \\\\ (\\forall i, x i ∈ I i) \\to (\\forall i, x i ∈ I i) \\to \\exists C' \\subseteq (J ∪ ⋃ i, I i) \\setminus range x, M.IsCircuit C' ∧ z ∈ C'$$$
Lean4
/-- A version of `Matroid.IsCircuit.strong_multi_elimination` that is phrased using insertion. -/
theorem strong_multi_elimination_insert (x : ι → α) (I : ι → Set α) (z : α) (hxI : ∀ i, x i ∉ I i)
(hC : ∀ i, M.IsCircuit (insert (x i) (I i))) (hJx : M.IsCircuit (J ∪ range x)) (hzJ : z ∈ J) (hzI : ∀ i, z ∉ I i) :
∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C' := by
-- we may assume that `ι` is nonempty, and it suffices to show that
-- `z` is spanned by the union of the `I` and `J \ {z}`.
obtain hι | hι := isEmpty_or_nonempty ι
· exact ⟨J, by simp, by simpa [range_eq_empty] using hJx, hzJ⟩
suffices hcl : z ∈ M.closure ((⋃ i, I i) ∪ (J \ { z }))
by
rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl
obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
refine ⟨C', ?_, hC', hzC'⟩
rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
have hC' (i) : M.closure (I i) = M.closure (insert (x i) (I i)) := by
simpa [diff_singleton_eq_self (hxI _)] using
(hC i).closure_diff_singleton_eq
(x i)
-- This is true because each `I i` spans `x i` and `(range x) ∪ (J \ {z})` spans `z`.
rw [closure_union_congr_left <| closure_iUnion_congr _ _ hC', iUnion_insert_eq_range_union_iUnion, union_right_comm]
refine
mem_of_mem_of_subset (hJx.mem_closure_diff_singleton_of_mem (.inl hzJ))
(M.closure_subset_closure (subset_trans ?_ subset_union_left))
rw [union_diff_distrib, union_comm]
exact union_subset_union_left _ diff_subset
