inv — Mathlib

English

If h: EventuallyConst f l and an inverse on β exists, then EventuallyConst f⁻¹ l.

Русский

Если f является EventuallyConst вдоль l и существует обратная функция на β, то f⁻¹ также EventuallyConst вдоль l.

LaTeX

$$$\mathrm{EventuallyConst}(f,l) \Rightarrow \mathrm{EventuallyConst}(f^{-1},l)$$$

Lean4

@[to_additive]
protected theorem inv [Inv β] (h : EventuallyConst f l) : EventuallyConst (f⁻¹) l :=
  h.comp Inv.inv

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