inject_dummies — Mathlib

English

If f,g, inv, p, and h are given as in the statement, there exists q such that ∀ v, S v ↔ ∃ t, q(v ⊗ t) = 0.

Русский

Если даны f, g, inv, p и h согласно утверждению, существует q, что ∀ v, S v ⇔ ∃ t, q(v ⊗ t) = 0.

LaTeX

$$$$ \\exists q : Poly (\\alpha ⊕ \\gamma), \\forall v, S v \\iff \\exists t, q(v \\otimes t) = 0 $$$$

Lean4

theorem inject_dummies (f : β → γ) (g : γ → Option β) (inv : ∀ x, g (f x) = some x) (p : Poly (α ⊕ β))
    (h : ∀ v, S v ↔ ∃ t, p (v ⊗ t) = 0) : ∃ q : Poly (α ⊕ γ), ∀ v, S v ↔ ∃ t, q (v ⊗ t) = 0 :=
  ⟨p.map (inl ⊗ inr ∘ f), fun v => (h v).trans <| inject_dummies_lem f g inv _ _⟩

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