range_pullbackSnd

Mathlib.CategoryTheory.Limits.Types.Pullbacks

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Types.range_pullbackSnd

English

Similarly, the range of pullback snd equals the preimage under g of the range of f.

Русский

Аналогично, образ pullback snd равен обратному образу g от образ f.

LaTeX

$$$\text{range}(\text{pullback}.snd f g) = g^{-1}(\text{range}(f)).$$$

Lean4

@[simp]
theorem range_pullbackSnd : Set.range (pullback.snd f g) = g ⁻¹' Set.range f :=
  range_snd_of_isPullback (.of_hasPullback f g)

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

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

Разделы

Аффилиация

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