finitary_iff_forall_isCircuit_finite

English

A matroid is finitary iff every circuit is finite.

Русский

Матроид финитар iff каждый цикл конечен.

LaTeX

$$$M.Finitary \\iff \\forall C, M.IsCircuit C \\rightarrow C.Finite$$$

Lean4

theorem finitary_iff_forall_isCircuit_finite : M.Finitary ↔ ∀ C, M.IsCircuit C → C.Finite :=
  by
  refine ⟨fun _ _ ↦ IsCircuit.finite, fun h ↦ ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_, fun x hx ↦ ?_⟩⟩⟩
  · obtain ⟨C, hCI, hC⟩ := hd.exists_isCircuit_subset
    exact hC.dep.not_indep <| hI _ hCI (h C hC)
  simpa using (hI { x } (by simpa) (finite_singleton _)).subset_ground

Похожие утверждения