evalFacProp — Mathlib

English

Let l be a product, J a predicate on I, and h a hypothesis saying J holds on all indices in l. Then the evaluation after restricting to J equals the unrestricted evaluation.

Русский

Пусть l — произведение, J — предикат на I, и h: ∀a, a ∈ l.val → J a. Тогда оценка после ограничения к J равна общей оценке.

LaTeX

$$$\\forall J\\, h,\\ (l.eval(\\pi C J) \\circ \\mathrm{ProjRestrict} C J) = l.eval C.$$$

Lean4

theorem evalFacProp {l : Products I} (J : I → Prop) (h : ∀ a, a ∈ l.val → J a) [∀ j, Decidable (J j)] :
    l.eval (π C J) ∘ ProjRestrict C J = l.eval C := by
  ext x
  dsimp [ProjRestrict]
  rw [Products.eval_eq, Products.eval_eq]
  simp +contextual [h, Proj]

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