eq_of_superset_spanning — Mathlib

English

If B is a base and X ⊆ B with X spanning, then B = X.

Русский

Если B база и X ⊆ B и X порождает, то B = X.

LaTeX

$$$$ hB: M.IsBase B \land hX: M.Spanning X \land hXB: X \subseteq B \Rightarrow B = X. $$$$

Lean4

theorem eq_of_superset_spanning (hB : M.IsBase B) (hX : M.Spanning X) (hXB : X ⊆ B) : B = X :=
  have ⟨B', hB', hB'X⟩ := hX.exists_isBase_subset
  subset_antisymm (by rwa [← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)]) hXB

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