restrictFreeVar — Mathlib

English

Restricting a bounded formula to a chosen set of free variables yields a new bounded formula whose free variables are a subset of the original, with a canonical way to map variable indices.

Русский

Ограничение свободных переменных формулы даёт новую ограниченную формулу с тем же смыслом, чьи свободные переменные подмножество оригинала.

LaTeX

$$$\text{restrictFreeVar} :\; L.BoundedFormula α n \to (φ.freeVarFinset \to β) \to L.BoundedFormula β n$ with the property that restricting maps variables along the injection of the chosen subset.$$

Lean4

/-- Restricts a bounded formula to only use a particular set of free variables. -/
def restrictFreeVar [DecidableEq α] :
    ∀ {n : ℕ} (φ : L.BoundedFormula α n) (_f : φ.freeVarFinset → β), L.BoundedFormula β n
  | _n, falsum, _f => falsum
  | _n, equal t₁ t₂, f =>
    equal (t₁.restrictVarLeft (f ∘ Set.inclusion subset_union_left))
      (t₂.restrictVarLeft (f ∘ Set.inclusion subset_union_right))
  | _n, rel R ts, f =>
    rel R fun i =>
      (ts i).restrictVarLeft
        (f ∘ Set.inclusion (subset_biUnion_of_mem (fun i => Term.varFinsetLeft (ts i)) (mem_univ i)))
  | _n, imp φ₁ φ₂, f =>
    (φ₁.restrictFreeVar (f ∘ Set.inclusion subset_union_left)).imp
      (φ₂.restrictFreeVar (f ∘ Set.inclusion subset_union_right))
  | _n, all φ, f => (φ.restrictFreeVar f).all

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