eq_emptyOn_or_nonempty

Mathlib.Combinatorics.Matroid.Constructions

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

← MathLib Explorer

English

A matroid is either emptyOn α or nonempty.

Русский

Матроид либо равен emptyOn α, либо непустой.

LaTeX

$$$ M = emptyOn(α) \\lor Matroid.Nonempty M $$$

Lean4

theorem eq_emptyOn_or_nonempty (M : Matroid α) : M = emptyOn α ∨ Matroid.Nonempty M :=
  by
  rw [← ground_eq_empty_iff]
  exact M.E.eq_empty_or_nonempty.elim Or.inl (fun h ↦ Or.inr ⟨h⟩)

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

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

Разделы

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

Аффилиация

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