indep_iff_forall_finite_subset_indep

English

In a finitary matroid, I is independent iff every finite J ⊆ I is independent.

Русский

В финитной матроидe I независимо тогда и только тогда, когда каждый конечный подмножество J ⊆ I независимо.

LaTeX

$$M.Indep(I) ↔ ∀ J ⊆ I, J.Finite → M.Indep(J)$$

Lean4

theorem indep_iff_forall_finite_subset_indep {M : Matroid α} [Finitary M] :
    M.Indep I ↔ ∀ J, J ⊆ I → J.Finite → M.Indep J :=
  ⟨fun h _ hJI _ ↦ h.subset hJI, Finitary.indep_of_forall_finite I⟩

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