supp_eq — Mathlib

English

The i-th support of x equals the set of u such that for every representation ⟨a,f⟩ of x, u ∈ f i '' univ.

Русский

Опора по i-й координате x совпадает с множеством u, для которого во всех представлениях ⟨a,f⟩ x выполняется u ∈ f i '' univ.

LaTeX

$$$$ \\mathrm{supp}\\ x\\ i = \\{ u \\mid \\forall a,f,\\ \\mathrm{abs}\\langle a,f\\rangle = x \\rightarrow u \\in f\\ i'' univ \\} $$$$

Lean4

theorem supp_eq {α : TypeVec n} {i} (x : F α) : supp x i = {u | ∀ a f, abs ⟨a, f⟩ = x → u ∈ f i '' univ} := by ext;
  apply mem_supp

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