subtypeDomain_def — Mathlib

English

The subtype-domain formed by restricting a DFinsupp to those indices satisfying p has a canonical representation mk with the restricted support and the corresponding coordinates.

Русский

Область подмножества, полученная ограничением DFinsupp к индексам, удовлетворяющим p, имеет каноническое представление mk с ограниченной опорой и соответствующими координатами.

LaTeX

$$$\\mathrm{subtypeDomain}\\;p\\ f = \\mathrm{mk}(f.{\\mathrm{support}}.\\mathrm{subtype}\\ p)\\; (\\lambda i, f i)$$$

Lean4

theorem subtypeDomain_def (f : Π₀ i, β i) : f.subtypeDomain p = mk (f.support.subtype p) fun i => f i := by ext i;
  by_cases h2 : f i ≠ 0 <;> try simp at h2; simp [h2]

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