ι_def — Mathlib

English

Another facet of the equality between lof and the composition with DirectSum.lof and ι'.

Русский

Ещё одно выражение равенства между lof и композицией с DirectSum.lof и ι'.

LaTeX

$$$\text{(restate of } lof = iota'\circ DirectSum.lof)$$$

Lean4

theorem ι_def : eta_helper Eq✝ @ι.{} @(delta% @definition✝) :=
  by
  intros
  delta ι
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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