isBasis_iff' — Mathlib

English

A basis criterion: I is a basis of X if and only if I is independent, I ⊆ X, and every independent J with I ⊆ J ⊆ X satisfies I = J, and X ⊆ E.

Русский

Критерий базы: I является базисом X тогда и только тогда, когда I независим, I ⊆ X, и любой независимый J с I ⊆ J ⊆ X удовлетворяет I = J, и X ⊆ E.

LaTeX

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

Lean4

theorem isBasis_iff' : M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E :=
  by
  rw [IsBasis, maximal_subset_iff]
  tauto

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