ratio_inv

Mathlib.Topology.MetricSpace.DilationEquiv

URI: https://scilib.ai/kg/mathlib#DilationEquiv.ratio_inv

English

Taking a natural power commutes with ratio: ratio(e^n) = (ratio e)^n.

Русский

Степенная мощность сохраняет отношение: ratio(e^n) = (ratio e)^n.

LaTeX

$$$\forall e : X \simeq^{\mathrm{d}} X,\ \forall n \in \mathbb{N},\ \operatorname{ratio}(e^n) = (\operatorname{ratio}(e))^n$$$

Lean4

@[simp]
theorem ratio_inv (e : X ≃ᵈ X) : ratio (e⁻¹) = (ratio e)⁻¹ :=
  ratio_symm e

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru