h_apply_fromCoset' — Mathlib

English

A variant of the previous fixed-coset property: for a chosen b ∈ B and its membership to the range, h(x)(fromCoset⟨b•range, b⟩) = fromCoset⟨b•range, b⟩.

Русский

Вариант фиксированной косеты: для выбранного b ∈ B и членства в диапазоне, имеет место h(x)(fromCoset⟨b·range, b⟩) = fromCoset⟨b·range, b⟩.

LaTeX

$$$$ h(x)\big(\mathrm{fromCoset}\langle b \cdot \operatorname{range}(f), b, rfl \rangle\big) = \mathrm{fromCoset}\langle b \cdot \uparrow\operatorname{range}(f), b, rfl \rangle. $$$$

Lean4

theorem h_apply_fromCoset' (x : B) (b : B) (hb : b ∈ f.hom.range) :
    h x (fromCoset ⟨b • f.hom.range, b, rfl⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
  (fromCoset_eq_of_mem_range _ hb).symm ▸ h_apply_fromCoset f x

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