h_apply_fromCoset — Mathlib

English

For x ∈ A, h(x) fixes the distinguished coset fromCoset⟨range(f),1⟩: (h x)(fromCoset⟨range(f),1⟩) = fromCoset⟨range(f),1⟩.

Русский

Для каждого x ∈ A, h(x) фиксирует выделенную косету fromCoset⟨range(f),1⟩: (h x)(fromCoset⟨range(f),1⟩) = fromCoset⟨range(f),1⟩.

LaTeX

$$$$ (h(x))(\mathrm{fromCoset}\left\langle \operatorname{range}(f), 1, 1_{\text{leftCoset}} \right\rangle) = \mathrm{fromCoset}\left\langle \operatorname{range}(f), 1, 1_{\text{leftCoset}} \right\rangle. $$$$

Lean4

theorem h_apply_fromCoset (x : B) :
    (h x) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ :=
  by
  change ((τ).symm.trans (g x)).trans τ _ = _
  simp [-MonoidHom.coe_range, τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]

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