evalFacProps — Mathlib

English

For l ∈ Products I, predicates J, K with hJK: J i → K i, and J ≤ K pointwise, the composed evaluations via restriction coincide: l.eval(π C J) ∘ ProjRestricts C hJK = l.eval(π C K).

Русский

Для l ∈ Products I и предикатов J, K с hJK: J i → K i, выполняется равенство $l.eval(π C J) ∘ ProjRestricts C hJK = l.eval(π C K)$.

LaTeX

$$$l.eval(π C J) \\circ ProjRestricts C hJK = l.eval(π C K).$$$

Lean4

theorem evalFacProps {l : Products I} (J K : I → Prop) (h : ∀ a, a ∈ l.val → J a) [∀ j, Decidable (J j)]
    [∀ j, Decidable (K j)] (hJK : ∀ i, J i → K i) : l.eval (π C J) ∘ ProjRestricts C hJK = l.eval (π C K) :=
  by
  have : l.eval (π C J) ∘ Homeomorph.setCongr (proj_eq_of_subset C J K hJK) = l.eval (π (π C K) J) := by ext;
    simp [Homeomorph.setCongr, Products.eval_eq]
  rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]

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