τ_apply_fromCoset' — Mathlib

English

If x ∈ range(f.hom), then τ(fromCoset⟨x • range(f.hom), x⟩) = ∞; i.e. τ sends cosets built from elements of the range to infinity.

Русский

Если x принадлежит образу f.hom, то τ(fromCoset⟨x • range(f.hom), x⟩) = ∞; то есть τ переводит косеты, составленные из элементов образа, в бесконечность.

LaTeX

$$$$ \tau\left(\mathrm{fromCoset}\left\langle x \cdot \operatorname{range}(f), x \right\rangle\right) = \infty, \quad \text{если } x \in \operatorname{range}(f). $$$$

Lean4

theorem τ_apply_fromCoset' (x : B) (hx : x ∈ f.hom.range) : τ (fromCoset ⟨x • ↑f.hom.range, ⟨x, rfl⟩⟩) = ∞ :=
  (fromCoset_eq_of_mem_range _ hx).symm ▸ τ_apply_fromCoset _

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