comap_finitary — Mathlib

English

If N is finitary, then the comap of N by f is finitary.

Русский

Если N является конечномерным по независимостям, то его комап по f тоже конечномерный.

LaTeX

$$N.Finitary \Rightarrow (N.comap f).Finitary$$

Lean4

instance comap_finitary (N : Matroid β) [N.Finitary] (f : α → β) : (N.comap f).Finitary :=
  by
  refine ⟨fun I hI ↦ ?_⟩
  rw [comap_indep_iff, indep_iff_forall_finite_subset_indep]
  simp only [forall_subset_image_iff]
  refine ⟨fun J hJ hfin ↦ ?_, fun x hx y hy ↦ (hI _ (pair_subset hx hy) (by simp)).2 (by simp) (by simp)⟩
  obtain ⟨J', hJ'J, hJ'⟩ := (surjOn_image f J).exists_bijOn_subset
  rw [← hJ'.image_eq] at hfin ⊢
  exact (hI J' (hJ'J.trans hJ) (hfin.of_finite_image hJ'.injOn)).1

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