proj' — Mathlib

English

A backward variant of projection: semilinearity of a predicate’s pushforward implies semilinearity of its existential form.

Русский

Обратная версия проекции: семилинейность предиката через конструкцию воспроизводится через существование.

LaTeX

$$$IsSemilinearSet(\{x \mid p( x \circ Sum.inl)(x \circ Sum.inr)\}) \Rightarrow IsSemilinearSet(\{x \mid \exists y, p x y\}).$$$

Lean4

/-- A variant of `Semilinear.proj` for backward reasoning. -/
theorem proj' {p : (ι → M) → (κ → M) → Prop} :
    IsSemilinearSet {x | p (x ∘ Sum.inl) (x ∘ Sum.inr)} → IsSemilinearSet {x | ∃ y, p x y} :=
  proj

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