comapOn_isBase_iff — Mathlib

English

A base of the comapOn matroid corresponds to a basis image in N together with injectivity and subset constraints: (N.comapOn E f).IsBase B iff N.IsBasis'(f''B) (f''E) ∧ InjOn f B ∧ B ⊆ E.

Русский

База матроида comapOn эквивалентна базе в N образе через f с инъективностью на B и включением B в E: (N.comapOn E f).IsBase B эквивалентно N.IsBasis'(f(B)) (f(E)) ∧ InjOn f B ∧ B ⊆ E.

LaTeX

$$$ (N.comapOn E f).IsBase B \iff N.IsBasis'(f''B) (f''E) \land B.InjOn f \land B \subseteq E $$$

Lean4

theorem comapOn_isBase_iff : (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ B.InjOn f ∧ B ⊆ E := by
  rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]

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