varFinsetLeft — Mathlib

English

For a function term, varFinset equals the union of the varFinsets of its argument terms.

Русский

Для терма-функции равенство: множество переменных функции равно объединению множеств переменных её аргументов.

LaTeX

$$$ (\text{varFinset} \; (\text{Term.func } F \ ts)) = \bigcup_{i} (\text{varFinset}(ts(i))) $$$

Lean4

/-- The `Finset` of variables from the left side of a sum used in a given term. -/
@[simp]
def varFinsetLeft [DecidableEq α] : L.Term (α ⊕ β) → Finset α
  | var (Sum.inl i) => { i }
  | var (Sum.inr _i) => ∅
  | func _f ts => univ.biUnion fun i => (ts i).varFinsetLeft

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