comp_injective

Mathlib.Topology.LocallyFinite

URI: https://scilib.ai/kg/mathlib#LocallyFinite.comp_injective

English

If f is locally finite and g is injective, then f ∘ g is locally finite.

Русский

Если f локально конечна и g инъективна, то f ∘ g локально конечна.

LaTeX

$$LocallyFinite f → Injective g → LocallyFinite (Function.comp f g)$$

Lean4

theorem comp_injective {g : ι' → ι} (hf : LocallyFinite f) (hg : Injective g) : LocallyFinite (f ∘ g) :=
  hf.comp_injOn hg.injOn

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

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

Разделы

Аффилиация

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