inter_eq_of_subset_indep — Mathlib

English

If I is a basis' of X, I ⊆ J, and J is independent, then J ∩ X = I.

Русский

Если I — IsBasis' множества X, и I ⊆ J, и J независимо, то J ∩ X = I.

LaTeX

$$$ (hI : M.IsBasis' I X) \\land (hIJ : I \\subseteq J) \\land hJ : M.Indep J \\Rightarrow J \\cap X = I $$$

Lean4

theorem inter_eq_of_subset_indep (hI : M.IsBasis' I X) (hIJ : I ⊆ J) (hJ : M.Indep J) : J ∩ X = I := by
  rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
    inter_eq_self_of_subset_left hJ.subset_ground]

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