freeOn_finitary — Mathlib

English

The matroid freeOn E is finitary; i.e., its independent sets satisfy the finitary condition.

Русский

Матроид freeOn(E) является конечностным; то есть независимые множества удовлетворяют финитарному условию.

LaTeX

$$$ (freeOn E).Finitary $$$

Lean4

instance freeOn_finitary : Finitary (freeOn E) :=
  by
  simp only [finitary_iff, freeOn_indep_iff]
  exact fun I h e heI ↦ by simpa using h { e } (by simpa)

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