freeVarFinset — Mathlib

English

The finite set of free variables of a bounded formula is defined recursively by the structure: falsum → ∅; equal t1 t2 → varFinsetLeft(t1) ∪ varFinsetLeft(t2); rel R ts → univ ⋃ ts i .varFinsetLeft; imp f1 f2 → freeVarFinset(f1) ∪ freeVarFinset(f2); all f → freeVarFinset(f).

Русский

Множество конечных свободных переменных ограничённой формулы определяется по структуре: falsum → ∅; equal t1 t2 → varFinsetLeft(t1) ∪ varFinsetLeft(t2); rel R ts → объединение по всем аргументам; imp f1 f2 → свободные переменные равны свободнымVarFinset(f1) ∪ свободнымVarFinset(f2); all f → свободныеVarFinset(f).

LaTeX

$$$\operatorname{freeVarFinset} (\text{falsum}) = \emptyset,\; \operatorname{freeVarFinset} (\text{equal } t_1 t_2) = \operatorname{varFinsetLeft}(t_1) \cup \operatorname{varFinsetLeft}(t_2),\; \operatorname{freeVarFinset} (\text{rel } R ts) = \bigcup_{i} \operatorname{varFinsetLeft}(ts(i)),\; \operatorname{freeVarFinset} (\text{imp } f_1 f_2) = \operatorname{freeVarFinset}(f_1) \cup \operatorname{freeVarFinset}(f_2),\; \operatorname{freeVarFinset} (\text{all } f) = \operatorname{freeVarFinset}(f).$$$

Lean4

/-- The `Finset` of free variables used in a given formula. -/
@[simp]
def freeVarFinset [DecidableEq α] : ∀ {n}, L.BoundedFormula α n → Finset α
  | _n, falsum => ∅
  | _n, equal t₁ t₂ => t₁.varFinsetLeft ∪ t₂.varFinsetLeft
  | _n, rel _R ts => univ.biUnion fun i => (ts i).varFinsetLeft
  | _n, imp f₁ f₂ => f₁.freeVarFinset ∪ f₂.freeVarFinset
  | _n, all f => f.freeVarFinset

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