leftInverse_invFun

Mathlib.MeasureTheory.MeasurableSpace.Embedding

URI: https://scilib.ai/kg/mathlib#MeasurableEmbedding.leftInverse_invFun

English

The inverse function hf.invFun is a left inverse to f, i.e., hf.invFun(f(x)) = x for all x.

Русский

Обратная функция hf.invFun является левосторонним обратным к f: hf.invFun(f(x)) = x для всякого x.

LaTeX

$$$\\forall x, \\ hf.invFun(f(x)) = x$$$

Lean4

theorem leftInverse_invFun [Nonempty α] (hf : MeasurableEmbedding f) : hf.invFun.LeftInverse f :=
  by
  intro x
  simp [MeasurableEmbedding.invFun]

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

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

Разделы

Аффилиация

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