base_injective — Mathlib

English

Reiterating the injectivity of the prod map from NormalWord to PushoutI φ in an alternative formulation.

Русский

Повторно изложено утверждение об инъективности отображения prod из NormalWord в PushoutI φ в другой формулировке.

LaTeX

$$$$\text{prod injective (alt)}.$$$$

Lean4

theorem base_injective (hφ : ∀ i, Function.Injective (φ i)) : Function.Injective (base φ) :=
  by
  rcases transversal_nonempty φ hφ with ⟨d⟩
  let _ := Classical.decEq ι
  let _ := fun i => Classical.decEq (G i)
  refine Function.Injective.of_comp (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_
  intro _ _ h
  exact eq_of_smul_eq_smul (fun w : NormalWord d => by simp_all [funext_iff, base_smul_eq_smul])

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