restrictSubtype_indep_iff_of_subset

English

If I ⊆ X, then independence in the restriction of M to X for I equals independence of I in M.

Русский

Если I ⊆ X, то независимость I в ограничении M к X равна независимости I в M.

LaTeX

$$$(M.restrictSubtype X).Indep(I) \iff M.Indep(I)$$$

Lean4

theorem restrictSubtype_indep_iff_of_subset (hIX : I ⊆ X) : (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I := by
  rw [restrictSubtype_indep_iff, image_preimage_eq_iff.2]; simpa

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