proj — Mathlib

English

Projections of semilinear sets along a sum decomposition are semilinear.

Русский

Проекции семилинейных множеств сохраняют семилинейность.

LaTeX

$$$IsSemilinearSet(s) \Rightarrow IsSemilinearSet(\{x \mid \exists y, Sum.elim x y \in s\}).$$$

Lean4

/-- Semilinear sets are closed under projection (from `ι ⊕ κ → M` to `ι → M` by taking `Sum.inl` on
the index). It is a special case of `IsSemilinearSet.image`. -/
theorem proj {s : Set (ι ⊕ κ → M)} (hs : IsSemilinearSet s) : IsSemilinearSet {x | ∃ y, Sum.elim x y ∈ s} :=
  by
  convert hs.image (LinearMap.funLeft ℕ M Sum.inl)
  ext x
  constructor
  · intro ⟨y, hy⟩
    exact ⟨Sum.elim x y, hy, rfl⟩
  · rintro ⟨y, hy, rfl⟩
    refine ⟨y ∘ Sum.inr, ?_⟩
    simpa [LinearMap.funLeft]

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