isBasis_self

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.isBasis_self

English

A basis I of I is equivalent to I being independent.

Русский

База I саму себя является независимой тогда и только тогда, когда I независима.

LaTeX

$$$ M.IsBasis I I \iff M.Indep I $$$

Lean4

theorem isBasis_self (h : M.Indep I) : M.IsBasis I I :=
  isBasis_self_iff_indep.mpr h

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

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

Разделы

Аффилиация

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