eq_of_subset_indep — Mathlib

English

If I is a Basis' I X, then I is the unique independent maximal subset of X containing I, equivalently I is the same as J under the independence relation with J ⊆ X.

Русский

Если I является Basis' I X, тогда I является уникальным максимальным независимым подмножеством X, равного J при J ⊆ X и независимости.

LaTeX

$$$ M.IsBasis' I X \rightarrow \forall J\, (M.Indep J \land I \subseteq J \land J \subseteq X \rightarrow I = J) $$$

Lean4

theorem eq_of_subset_indep (hI : M.IsBasis' I X) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X) : I = J :=
  hIJ.antisymm (hI.2 ⟨hJ, hJX⟩ hIJ)

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