ofEquiv — Mathlib

English

Transport a FinEnum instance across an equivalence h: β ≃ α to obtain a FinEnum β with the same cardinality as α.

Русский

Переносим FinEnum через эквивалентность h: β ≃ α, чтобы получить FinEnum β с той же мощностью, что и α.

LaTeX

$$$\\operatorname{ofEquiv}(α)\\; (β) [FinEnum α] (h: β\\simeq α) : FinEnum β$$$

Lean4

/-- transport a `FinEnum` instance across an equivalence -/
def ofEquiv (α) {β} [FinEnum α] (h : β ≃ α) : FinEnum β
    where
  card := card α
  equiv := h.trans (equiv)
  decEq := (h.trans (equiv)).decidableEq

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