indep

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.indep

English

If B is a base, then B is independent.

Русский

Если B является базой, то B независим.

LaTeX

$$$ M.IsBase B \Rightarrow M.Indep B $$$

Lean4

theorem indep (hB : M.IsBase B) : M.Indep B :=
  indep_iff.2 ⟨B, hB, subset_rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru