constantsOnMap_isExpansionOn — Mathlib

English

The expansion map lhomWithConstants α is injective.

Русский

Расширение линейного гомоморфизма с константами инъективно.

LaTeX

$$$ (L.lhomWithConstants α).Injective $$$

Lean4

theorem constantsOnMap_isExpansionOn {f : α → β} {fα : α → M} {fβ : β → M} (h : fβ ∘ f = fα) :
    @LHom.IsExpansionOn _ _ (LHom.constantsOnMap f) M (constantsOn.structure fα) (constantsOn.structure fβ) :=
  by
  letI := constantsOn.structure fα
  letI := constantsOn.structure fβ
  exact ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F :)) fun n F => isEmptyElim F, fun R => isEmptyElim R⟩

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