equiv'_symm_apply — Mathlib

English

Applying the constructor equivalence to a vector i yields the mapped vector: b.equiv' b' f g hf hg hgf hfg (b i) = f(b i).

Русский

При применении эквивалентности конструирования вектору i получаем соответственный вектор: b.equiv' b' f g ... (b i) = f(b i).

LaTeX

$$$b.\\mathrm{equiv'}\\; b'\\; f\\; g\\; hf\\; hg\\; hgf\\; hfg (b i) = f(b i).$$$

Lean4

@[simp]
theorem equiv'_symm_apply (f : M → M') (g : M' → M) (hf hg hgf hfg) (i : ι') :
    (b.equiv' b' f g hf hg hgf hfg).symm (b' i) = g (b' i) :=
  b'.constr_basis R _ _

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