comapOn_indep_iff — Mathlib

English

Let f: α → β, E ⊆ α, I ⊆ α, and N be a matroid on β. Then I is independent in the comapOn matroid N ∘ f on E exactly when I ⊆ E, f is injective on I, and the image f(I) is independent in N.

Русский

Пусть f: α → β, E ⊆ α, I ⊆ α и N — матроид на β. Тогда I является независимым в матроидe comapOn, полученном из N через f на E, тогда и только тогда I ⊆ E, f инъективна на I, и образ f(I) независим в N.

LaTeX

$$$ (N\mid_{E}^{f}) \ Indep(I) \quad\Longleftrightarrow\quad (N.Indep(f(I)) \land InjOn(f,I) \land I \subseteq E). $$$

Lean4

@[simp]
theorem comapOn_indep_iff : (N.comapOn E f).Indep I ↔ (N.Indep (f '' I) ∧ InjOn f I ∧ I ⊆ E) := by
  simp [comapOn, and_assoc]

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