eq

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.LeftInvOn.eq

English

If h is a left inverse on s, then for any x in s, f'(f(x)) = x.

Русский

Если h задаёт левый обратный на s, то для любого x ∈ s выполнено f'(f(x)) = x.

LaTeX

$$$$ \\text{If } h : \\text{LeftInvOn } f' f s, \\; x \\in s \\Rightarrow f'(f(x)) = x. $$$$

Lean4

theorem eq (h : LeftInvOn f' f s) {x} (hx : x ∈ s) : f' (f x) = x :=
  h hx

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

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

Разделы

Аффилиация

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