freeOn_empty

Mathlib.Combinatorics.Matroid.Constructions

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

English

freeOn of the empty set equals the empty matroid on the ambient type.

Русский

freeOn пустого множества совпадает с пустым матроидом на заданном множестве.

LaTeX

$$$ \\text{freeOn}(\\emptyset) = \\text{emptyOn} $$$

Lean4

@[simp]
theorem freeOn_empty (α : Type*) : freeOn (∅ : Set α) = emptyOn α := by simp [freeOn]

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

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

Разделы

Аффилиация

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