matroid_spanning_iff — Mathlib

English

For any s ⊆ A, the matroid spanning s is equivalent to A being algebraic over adjoin_R s; i.e., the whole algebra A is algebraic over the adjoin of s if and only if s spans A in the matroid sense.

Русский

Для любого подмножества s ⊆ A, спаннинг матроида s равносилен тому, что A алгебраично над adjoin_R s.

LaTeX

$$$ (\\mathrm{matroid} \\; R\\, A).Spanning(s) \\iff \\mathrm{Algebra.IsAlgebraic}(\\operatorname{adjoin}_R s)\\ A $$$

Lean4

theorem matroid_spanning_iff [IsDomain A] {s : Set A} : (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (adjoin R s) A :=
  by
  simp_rw [Matroid.spanning_iff, matroid_e, subset_univ, and_true, eq_univ_iff_forall, matroid_closure_eq,
    SetLike.mem_coe, mem_algebraicClosure, Algebra.isAlgebraic_def]

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