English
Generalization where the collection of circuits is a Set of Sets S and the distinguished elements form a set X; under suitable hypotheses there exists C' ⊆ (C0 ∪ ⋃ S) \\ X which is a circuit and contains z.
Русский
Обобщение, когда коллекция окружностей — это множество множеств S, и distinguished элементы образуют множество X; при заданных гипотезах существует C' ⊆ (C0 ∪ ⋃ S) \\ X, такая что C' — окружность и z ∈ C'.
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, \\exists C ∈ S, C ∩ X = { x }) \\to z ∈ C_0 \\to (\\forall C ∈ S, z ∉ C) \\to ∃ C' ⊆ (C_0 ∪ ⋃₀ S) \\setminus X, M.IsCircuit C' ∧ z ∈ C'$$$
Lean4
/-- A version of `Circuit.strong_multi_elimination` where the collection of circuits is
a `Set (Set α)` and the distinguished elements are a `Set α`, rather than both being indexed. -/
theorem strong_multi_elimination_set (hC₀ : M.IsCircuit C₀) (X : Set α) (S : Set (Set α)) (z : α)
(hCS : ∀ C ∈ S, M.IsCircuit C) (hXC₀ : X ⊆ C₀) (hX : ∀ x ∈ X, ∃ C ∈ S, C ∩ X = { x }) (hzC₀ : z ∈ C₀)
(hz : ∀ C ∈ S, z ∉ C) : ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C' :=
by
choose! C hC using hX
simp only [forall_and] at hC
have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
· obtain ⟨C', hC'ss, hC', hz⟩ := hwin
refine ⟨C', hC'ss.trans (diff_subset_diff (union_subset_union_right _ ?_) (by simp)), hC', hz⟩
simpa using fun e heX ↦ (subset_sUnion_of_mem (hC.1 e heX))
· simpa using fun e heX ↦ hCS _ <| hC.1 e heX
· simpa using fun e heX ↦ hXC₀ heX
· simp only [Subtype.forall, ← singleton_subset_iff (s := C _)]
exact fun e heX ↦ by simp [← hC.2 e heX]
· simp only [Subtype.forall, Subtype.mk.injEq]
refine fun e heX f hfX hef ↦ ?_
simpa [hC.2 f hfX] using subset_inter (singleton_subset_iff.2 hef) (singleton_subset_iff.2 heX)
simpa using fun e heX heC ↦ hz _ (hC.1 e heX) heC
