apply_rangeSplitting

Mathlib.Data.Set.Operations

URI: https://scilib.ai/kg/mathlib#Set.apply_rangeSplitting

English

Let f: A → B and x ∈ range(f). Then f(rangeSplitting(f)(x)) = x.

Русский

Пусть f: A → B и x ∈ range(f). Тогда f(rangeSplitting(f)(x)) = x.

LaTeX

$$$$\\forall f:\\alpha \\to \\beta,\\; \\forall x\\in \\mathrm{range}(f),\\; f(\\mathrm{rangeSplitting}(f)(x)) = x.$$$$

Lean4

theorem apply_rangeSplitting (f : α → β) (x : range f) : f (rangeSplitting f x) = x :=
  x.2.choose_spec

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

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

Разделы

Аффилиация

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