equiv_fst_eq_mul_inv — Mathlib

English

Let φ: S × T → G be the bijection given by φ(s,t) = s t. Then for each g ∈ G, if φ(g) = (s,t) then s = g t^{-1}. In particular, the first coordinate is determined by g and t.

Русский

Пусть φ: S × T → G — биекция, заданная φ(s,t) = s t. Тогда для каждого g ∈ G, если φ(g) = (s,t), то s = g t^{-1}. В частности, первая координата определяется по g и t.

LaTeX

$$$\forall g\in G:\; (\exists! (s,t)\in S\times T:\; g=s t)\Rightarrow s = g t^{-1}. $$$

Lean4

theorem equiv_fst_eq_mul_inv (g : G) : ↑(hST.equiv g).fst = g * ((hST.equiv g).snd : G)⁻¹ :=
  eq_mul_inv_of_mul_eq (hST.equiv_fst_mul_equiv_snd g)

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