loopyOn — Mathlib

English

The construction loopyOn(E) defines a matroid on α whose ground is E and whose only base is ∅; elements of E are loops.

Русский

Конструкция loopyOn(E) задаёт матроид на α с основанием ∅ и основанием E; элементы E — петли.

LaTeX

$$$\\mathrm{loopyOn}(E) = \\mathrm{emptyOn}(α) \\restriction E$$$

Lean4

/-- The `Matroid α` with ground set `E` whose only base is `∅`.
The elements are all 'loops' - see `Matroid.IsLoop` and `Matroid.loopyOn_isLoop_iff`. -/
def loopyOn (E : Set α) : Matroid α :=
  emptyOn α ↾ E

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