small_congr — Mathlib

English

Smallness is preserved along equivalences: if e: α ≃ β, then Small(α) ↔ Small(β).

Русский

Мелкость сохраняется при эквиваленциях: если e: α ≃ β, то Small(α) ↔ Small(β).

LaTeX

$$$Small(\alpha) \iff Small(\beta) \text{ for } e: \alpha \simeq \beta.$$$

Lean4

theorem small_congr {α : Type*} {β : Type*} (e : α ≃ β) : Small.{w} α ↔ Small.{w} β :=
  ⟨fun h => @small_map _ _ h e.symm, fun h => @small_map _ _ h e⟩

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