boundedFormula_realize_eq_realize

English

A simp-equivalent variant of the graph realization which states equality of the realized graph with the realized term equality.

Русский

Симп-эквивалентная формулировка реализации графа утверждает равенство реализованного графа и реализованного равенства термов.

LaTeX

$$$ \operatorname{Eq}((\text{graph } f)^M(\text{cons } y\; x), \operatorname{Eq}(\text{funMap } f\; x)\; y) $$$

Lean4

theorem boundedFormula_realize_eq_realize (φ : L.Formula α) (x : α → M) (y : Fin 0 → M) :
    BoundedFormula.Realize φ x y ↔ φ.Realize x :=
  by
  rw [Formula.Realize, iff_iff_eq]
  congr
  ext i; exact Fin.elim0 i

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