comp_injOn — Mathlib

English

If f is locally finite and g is such that g is injective on the indices where f(g(i)) is nonempty, then f ∘ g is locally finite.

Русский

Пусть f локально конечна и g такова, что на множестве индексов, где f(g(i)) непусто, g инъективна; тогда f ∘ g локально конечно.

LaTeX

$$LocallyFinite f → InjOn g {i | (f (g i)).Nonempty} → LocallyFinite (f ∘ g)$$

Lean4

theorem comp_injOn {g : ι' → ι} (hf : LocallyFinite f) (hg : InjOn g {i | (f (g i)).Nonempty}) :
    LocallyFinite (f ∘ g) := fun x => by
  let ⟨t, htx, htf⟩ := hf x
  refine ⟨t, htx, htf.preimage <| ?_⟩
  exact hg.mono fun i (hi : Set.Nonempty _) => hi.left

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