comp_right — Mathlib

English

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

Русский

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

LaTeX

$$IsLocallyInjective f \rightarrow (Continuous g ∧ g.Injective) \rightarrow IsLocallyInjective (f ∘ g)$$

Lean4

theorem comp_right {f : X → Y} (hf : IsLocallyInjective f) {g : A → X} (cont : Continuous g) (hg : g.Injective) :
    IsLocallyInjective (f ∘ g) := by
  rw [isLocallyInjective_iff_isOpen_diagonal] at hf ⊢
  rw [← hg.preimage_pullbackDiagonal]
  apply hf.preimage (cont.mapPullback cont)

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