right_inv — Mathlib

English

If f is an isometry and g is a right inverse of f (i.e., f ∘ g = id), then g is an isometry.

Русский

Если f — изометрия, и g является правым обратным к f (то есть f ∘ g = id), то g — изометрия.

LaTeX

$$$Isometry(f) \rightarrow RightInverse(g,f) \rightarrow Isometry(g)$$$

Lean4

/-- The right inverse of an isometry is an isometry. -/
theorem right_inv {f : α → β} {g : β → α} (h : Isometry f) (hg : RightInverse g f) : Isometry g := fun x y => by
  rw [← h, hg _, hg _]

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