left_inv_of_invOfMemRange

Mathlib.Data.Fintype.Inv

URI: https://scilib.ai/kg/mathlib#Function.Injective.left_inv_of_invOfMemRange

English

For any injective f, for every b in the range, f(invOfMemRange(b)) = b.

Русский

Для инъекции f для каждого b из образа выполняется f(invOfMemRange(b)) = b.

LaTeX

$$$ \\forall b:\\mathrm{Set.range}(f).\\, f(\\mathrm{invOfMemRange}(b)) = b $$$

Lean4

theorem left_inv_of_invOfMemRange (b : Set.range f) : f (hf.invOfMemRange b) = b :=
  (Finset.choose_spec (fun a => f a = b) _ _).right

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

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

Разделы

Аффилиация

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