freeOn_isBasis'_iff — Mathlib

English

Let E, I, X be subsets of the ambient set. In the matroid freeOn E, the relation that I is a basis of X (within freeOn E) holds exactly when I equals X ∩ E. In other words, the unique basis on X is X ∩ E.

Русский

Пусть E, I, X — подмножества исходного множества. В матроидe freeOn(E) множество I является базисом множества X тогда и только тогда, когда I равно X ∩ E. Другими словами, на множестве X базисом является именно X ∩ E.

LaTeX

$$$ (freeOn\, E).IsBasis'(I,X) \iff I = X \cap E $$$

Lean4

@[simp]
theorem freeOn_isBasis'_iff : (freeOn E).IsBasis' I X ↔ I = X ∩ E := by
  rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground, and_iff_left inter_subset_right]

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