g_ne_h — Mathlib

English

If there exists x ∈ B not in range(f.hom), then g ≠ h as monoid homs B → SX'.

Русский

Если существует x ∈ B, не принадлежащий образу f.hom, то g ≠ h как моноид-гомом B → SX'.

LaTeX

$$$$ g \neq h. $$$$

Lean4

theorem g_ne_h (x : B) (hx : x ∉ f.hom.range) : g ≠ h :=
  by
  intro r
  apply fromCoset_ne_of_nin_range _ hx
  replace r := DFunLike.congr_fun (DFunLike.congr_fun r x) (fromCoset ⟨f.hom.range, ⟨1, one_leftCoset _⟩⟩)
  simpa [g_apply_fromCoset, «h», tau, g_apply_infinity] using r

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