loopyOn_empty

Mathlib.Combinatorics.Matroid.Constructions

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

English

LoopyOn applied to the empty set equals the emptyOn matroid.

Русский

LoopyOn для пустого множества равен пустому основанию.

LaTeX

$$$\\text{loopyOn}(\\emptyset) = \\text{emptyOn}(\\alpha)$$$

Lean4

@[simp]
theorem loopyOn_empty (α : Type*) : loopyOn (∅ : Set α) = emptyOn α := by rw [← ground_eq_empty_iff, loopyOn_ground]

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

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

Разделы

Аффилиация

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