realize_foldr_imp — Mathlib

English

A related simp corollary gives that a fold by min over formulas corresponds to a universal condition.

Русский

Сопутствующее упрощение показывает, что свёртка через min над формулами соответствует всеобщему условию.

LaTeX

$$$ (l.foldr (\mathbf{min}) \top).Realize v xs \;\Longleftrightarrow\; \forall φ \in l, φ.Realize v xs $$$

Lean4

/-- List.foldr on BoundedFormula.imp gives a big "And" of input conditions. -/
theorem realize_foldr_imp {k : ℕ} (l : List (L.BoundedFormula α k)) (f : L.BoundedFormula α k) :
    ∀ (v : α → M) xs, (l.foldr BoundedFormula.imp f).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs) :=
  by
  intro v xs
  induction l
  next => simp
  next f' _ _ => by_cases f'.Realize v xs <;> simp [*]

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