varFinset — Mathlib

English

For a term t, varFinset(t) is the (finite) set of variables appearing in t; defined recursively by the structure of t.

Русский

Для терма t множество переменных, встречающихся в t, является сконструированным повторяемо конечным множеством, задаваемым по структуре терма.

LaTeX

$$$ \text{varFinset} : L.\text{Term } \alpha \to \text{Finset } \alpha $$$

Lean4

/-- The `Finset` of variables used in a given term. -/
@[simp]
def varFinset [DecidableEq α] : L.Term α → Finset α
  | var i => { i }
  | func _f ts => univ.biUnion fun i => (ts i).varFinset

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