τ_symm_apply_fromCoset — Mathlib

English

The inverse of τ takes the left coset determined by range(f) back to ∞, i.e. τ^{-1}(fromCoset(⟨range(f),1⟩)) = ∞.

Русский

Обратный переход τ переводит левую косету, заданную диапазоном образа, обратно в ∞: τ^{-1}(fromCoset(⟨range(f),1⟩)) = ∞.

LaTeX

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

Lean4

theorem τ_symm_apply_fromCoset : Equiv.symm τ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = ∞ := by
  rw [tau, Equiv.symm_swap, Equiv.swap_apply_left]

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