exists_isBase — Mathlib

English

There exists B such that B is a base and I = B ∩ X.

Русский

Существует B такая, что B — база и I = B ∩ X.

LaTeX

$$$ \exists B, M.IsBase B \land I = B \cap X $$$

Lean4

theorem exists_isBase (hI : M.IsBasis I X) : ∃ B, M.IsBase B ∧ I = B ∩ X :=
  let ⟨B, hB, hIB⟩ := hI.indep.exists_isBase_superset
  ⟨B, hB,
    subset_antisymm (subset_inter hIB hI.subset)
      (by rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset) inter_subset_right])⟩

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