rec_equivShrink — Mathlib

English

The recursor of Shrink commutes with the equivalence: for every a in α, Shrink.rec f (equivShrink(α) a) = f(a).

Русский

Рекурсор Shrink совместим с эквивалентностью: для каждого a ∈ α, Shrink.rec f (equivShrink(α) a) = f(a).

LaTeX

$$$\mathrm{Shrink.rec}\, f\, (\mathrm{equivShrink}(\alpha)\, a) = f(a).$$$

Lean4

@[simp]
theorem rec_equivShrink {α : Type*} [Small.{w} α] {F : Shrink α → Sort v} {f : (a : α) → F (equivShrink α a)} (a : α) :
    Shrink.rec f (equivShrink _ a) = f a :=
  by
  simp only [Shrink.rec, eqRec_eq_cast, cast_eq_iff_heq]
  rw [Equiv.symm_apply_apply]

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