τ_apply_fromCoset — Mathlib

English

For any f: A → B, τ(fromCoset(⟨range(f), 1, leftCoset⟩)) = ∞, i.e. τ sends the coset determined by the range of f to the point at infinity.

Русский

Для любого f: A → B, τ(fromCoset(⟨range(f), 1, leftCoset⟩)) = ∞, то есть τ переводит косет, заданный образами f, в точку бесконечности.

LaTeX

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

Lean4

theorem τ_apply_fromCoset : τ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = ∞ :=
  Equiv.swap_apply_left _ _

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