eq_emptyOn

Mathlib.Combinatorics.Matroid.Constructions

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

English

If the type α is empty, then any matroid M on α equals emptyOn α.

Русский

Если тип α пуст, то любой матроид M на α равен emptyOn α.

LaTeX

$$$[IsEmpty(\\alpha)]\\ M = emptyOn(α)$$$

Lean4

theorem eq_emptyOn [IsEmpty α] (M : Matroid α) : M = emptyOn α :=
  by
  rw [← ground_eq_empty_iff]
  exact M.E.eq_empty_of_isEmpty

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

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

Разделы

Аффилиация

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