isLocallyInjective_iff_of_fac — Mathlib

English

Given φ, ψ with a factoring fac: φ ≫ ψ = φψ, IsLocallyInjective J φψ is equivalent to IsLocallyInjective J φ provided by the factoring, and conversely, if φψ is locally injective then φ is too after adjusting by fac.

Русский

При наличии разложения fac: φ ≫ ψ = φψ локальная инъективность φψ эквивалентна локальной инъективности φ, и наоборот при корректировке fac.

LaTeX

$$$fac: φ ≫ ψ = φψ \Rightarrow IsLocallyInjective(J, φψ) \iff IsLocallyInjective(J, φ)$$$

Lean4

theorem isLocallyInjective_iff_of_fac {φψ : F₁ ⟶ F₃} (fac : φ ≫ ψ = φψ) [IsLocallyInjective J ψ] :
    IsLocallyInjective J φψ ↔ IsLocallyInjective J φ :=
  by
  constructor
  · intro
    exact isLocallyInjective_of_isLocallyInjective_fac J fac
  · intro
    rw [← fac]
    infer_instance

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