English
If M is finitary, then M.map f hf is finitary.
Русский
Если M является конечно-дифференцируемым (finitary), то отображение M.map f hf тоже является finitary.
LaTeX
$$$ M.Finitary \Rightarrow (M.map f hf).Finitary $$$
Lean4
instance [M.Finitary] {f : α → β} (hf) : (M.map f hf).Finitary :=
by
refine ⟨fun I hI ↦ ?_⟩
simp only [map_indep_iff]
have h' : I ⊆ f '' M.E := by
intro e he
obtain ⟨I₀, hI₀, h_eq⟩ := hI { e } (by simpa) (by simp)
exact image_mono hI₀.subset_ground <| h_eq.subset rfl
obtain ⟨I₀, hI₀E, rfl⟩ := subset_image_iff.1 h'
refine ⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩
specialize hI (f '' J₀) (image_mono hJ₀I₀) (hJ₀.image _)
rwa [map_image_indep_iff (hJ₀I₀.trans hI₀E)] at hI
