inter_isBasis_sInter — Mathlib

English

Let I be independent in M and suppose Xs is a nonempty family of subsets. If for every X in Xs, X ∩ I is a basis of X, then (⋂ Xs) ∩ I is a basis for ⋂ Xs.

Русский

Пусть I независимо в M и Xs — ненулевое семейство подмножеств. Если для каждого X из Xs X ∩ I является базисом X, тогда ⋂ Xs ∩ I является базисом ⋂ Xs.

LaTeX

$$$\text{If } hI:\ M.Indep I,\ hXs:\ Xs.Nonempty,\ h:\ \forall X\\in Xs,\\ M.IsBasis(X\\cap I,X),\\\text{ then } M.IsBasis\\big((\\bigcap Xs)\\cap I\\big)\\big(\\bigcap Xs\\big).$$$

Lean4

theorem inter_isBasis_sInter {Xs : Set (Set α)} (hI : M.Indep I) (hXs : Xs.Nonempty)
    (h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X) : M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs) :=
  by
  rw [sInter_eq_biInter]
  exact hI.inter_isBasis_biInter hXs h

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