mk' — Mathlib

English

If a type e is denumerable and is given by an equivalence e : α ≃ ℕ, then Denumerable.mk' constructs a denumerable structure on α.

Русский

Если имеется эквивалентность e : α ≃ ℕ, то Denumerable.mk' создаёт денумерируемую структуру на α.

LaTeX

$$$ \text{mk'}(e) : \text{Denumerable } α $ with encode := e, decode := \text{Some} \circ e^{-1}$$$

Lean4

/-- A type equivalent to `ℕ` is denumerable. -/
def mk' {α} (e : α ≃ ℕ) : Denumerable α where
  encode := e
  decode := some ∘ e.symm
  encodek _ := congr_arg some (e.symm_apply_apply _)
  decode_inv _ := ⟨_, rfl, e.apply_symm_apply _⟩

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