contract_finitary — Mathlib

English

If M is finitary, then M / C is finitary.

Русский

Если M является конечнопосредственным, то и M / C так же.

LaTeX

$$$\\text{Finitary}(M) \\Rightarrow \\text{Finitary}(M / C)$$$

Lean4

instance contract_finitary [Finitary M] : Finitary (M ／ C) :=
  by
  obtain ⟨J, hJ⟩ := M.exists_isBasis' C
  suffices (M ／ J).Finitary by
    rw [hJ.contract_eq_contract_delete]
    infer_instance
  exact
    ⟨fun I hI ↦
      hJ.indep.contract_indep_iff.2
        ⟨disjoint_left.2 fun e heI ↦ ((hI { e } (by simpa) (by simp)).subset_ground rfl).2,
          indep_of_forall_finite_subset_indep _ fun K hK hKfin ↦
            (hJ.indep.contract_indep_iff.1 <| hI (K ∩ I) inter_subset_right (hKfin.inter_of_left _)).2.subset
              (by tauto_set)⟩⟩

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