ofEquiv — Mathlib

English

Denumerability is preserved by equivalences: if β ≃ α and α is denumerable, then β is denumerable.

Русский

Денумерируемость сохраняется при эквивалентностях: если β ≃ α и α денумерируем, то β денумеруем.

LaTeX

$$$ \text{ofEquiv }(\alpha){\beta} \ [Denumerable \alpha] (e : \beta \simeq \alpha) : Denumerable \beta $$$

Lean4

/-- Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable
way. -/
def ofEquiv (α) {β} [Denumerable α] (e : β ≃ α) : Denumerable β :=
  { Encodable.ofEquiv _ e with decode_inv := fun n => by simp [decode_ofEquiv, encode_ofEquiv] }

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