rangeFactorization_coe

Mathlib.Data.Set.Image

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

English

For any f and a, the a-th element of rangeFactorization f, when coerced to β, equals f a.

Русский

Для любой f и a элемент rangeFactorization f a при приведении к β равен f a.

LaTeX

$$$$ (\\operatorname{rangeFactorization} f\\, a : \\beta) = f\\, a $$$$

Lean4

@[simp]
theorem rangeFactorization_coe (f : ι → β) (a : ι) : (rangeFactorization f a : β) = f a :=
  rfl

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

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

Разделы

Аффилиация

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