unify — Mathlib

English

Unify raises a family of elements from the Σ-type to a common level along the embeddings, choosing a level i and transporting each x via its embedding to G_i.

Русский

Unify переводит семейство элементов из Σ-типа на общую ступеньку i вдоль вложений, переводя каждый элемент через соответствующее вложение к G_i.

LaTeX

$$$\\mathrm{unify}_f(x,i,h,a)=f\\big((x a).1\\big)\\big(i,(h\\circ\\mathrm{mem\\_range\\_self}(a)),(x a).2\\big)$$$

Lean4

/-- Raises a family of elements in the `Σ`-type to the same level along the embeddings. -/
def unify {α : Type*} (x : α → Σˣ f) (i : ι) (h : i ∈ upperBounds (range (Sigma.fst ∘ x))) (a : α) : G i :=
  f (x a).1 i (h (mem_range_self a)) (x a).2

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