restrict_finitary — Mathlib

English

If M is finitary, then the restriction M|R is also finitary.

Русский

Если M финитный, то ограничение M до R также финитное.

LaTeX

$$$ (M|R).Finitary $$$

Lean4

instance restrict_finitary [Finitary M] (R : Set α) : Finitary (M ↾ R) :=
  by
  refine ⟨fun I hI ↦ ?_⟩
  simp only [restrict_indep_iff] at *
  rw [indep_iff_forall_finite_subset_indep]
  exact ⟨fun J hJ hJfin ↦ (hI J hJ hJfin).1, fun e heI ↦ singleton_subset_iff.1 (hI _ (by simpa) (toFinite _)).2⟩

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