isBasis_ground_iff — Mathlib

English

A basis B constructed from ground E is equivalent to B being a base with ground E.

Русский

База B, построенная на массиве E, эквивалентна тому, что B является базой с опорным множеством E.

LaTeX

$$$ M.IsBasis B M.E \iff M.IsBase B $$$

Lean4

@[simp]
theorem isBasis_ground_iff : M.IsBasis B M.E ↔ M.IsBase B := by
  rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground), and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]

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