realize_foldr_inf — Mathlib

English

A fold over a list with an accumulation of implications yields a universal implication form: the fold equals a function that if all items hold then the final term holds.

Русский

Свёртка по списку с накоплением импликаций даёт унифицированную форму импликаций: свёртка эквивалентна импликации от всех элементов.

LaTeX

$$$ (l.foldr BoundedFormula.imp f l).Realize v xs = ((\forall i \in l, i.Realize v xs) \rightarrow f.Realize v xs) $$$

Lean4

@[simp]
theorem realize_foldr_inf (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) :
    (l.foldr (· ⊓ ·) ⊤).Realize v xs ↔ ∀ φ ∈ l, BoundedFormula.Realize φ v xs := by
  induction l with
  | nil => simp
  | cons φ l ih => simp [ih]

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