freeOn_isBase_iff

Mathlib.Combinatorics.Matroid.Constructions

URI: https://scilib.ai/kg/mathlib#Matroid.freeOn_isBase_iff

← MathLib Explorer

English

(freeOn(E)).IsBase B if and only if B = E.

Русский

База матроида freeOn(E) равна B тогда и только тогда, когда B = E.

LaTeX

$$$ (\\text{freeOn}(E)).IsBase B \\;\\Leftrightarrow\\; B = E $$$

Lean4

@[simp]
theorem freeOn_isBase_iff : (freeOn E).IsBase B ↔ B = E := by
  simp only [freeOn, loopyOn_ground, dual_isBase_iff', loopyOn_isBase_iff, diff_eq_empty, ← subset_antisymm_iff,
    eq_comm (a := E)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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