funMap_quotient_mk'_sigma_mk' — Mathlib

English

The funMap constructed on a quotient coincides with the direct representation of the quotient of Sigma.mk.

Русский

Функция funMap, построенная на фактор-множество, совпадает с прямым представлением квантизированного Sigma.mk.

LaTeX

$$$\\mathrm{funMap}_f \\big(\\lambda a. \\langle i, x(a)\\rangle\\big) = \\langle i, \\mathrm{funMap}_f(x)\\rangle$$$

Lean4

@[simp]
theorem funMap_quotient_mk'_sigma_mk' {n : ℕ} {F : L.Functions n} {i : ι} {x : Fin n → G i} :
    funMap F (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) = ⟦.mk f i (funMap F x)⟧ :=
  by
  simp only [funMap_quotient_mk', Quotient.eq]
  obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
  refine ⟨k, jk, ik, ?_⟩
  simp only [Embedding.map_fun, comp_unify]
  rfl

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