leftInvOn — Mathlib

English

If f has a left inverse g, then on any set s, the left inverse relation holds, i.e., g is a left inverse of f on s.

Русский

Пусть у функции f есть левый обратный g; на любом множестве s g остаётся левым обратным для f.

LaTeX

$$$\\text{LeftInverse}\; f\; g \\Rightarrow \\text{LeftInvOn}\; f\; g\; s$$$

Lean4

theorem leftInvOn {g : β → α} (h : LeftInverse f g) (s : Set β) : LeftInvOn f g s := fun x _ => h x

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