equiv_fst_mul_equiv_snd — Mathlib

English

Let S, T be a complement pair in G. For every g ∈ G there is a unique pair (s,t) ∈ S × T with g = s t; moreover, if we write φ(g) = (s,t) for the unique such pair, then φ(g) is a pair whose product equals g.

Русский

Пусть S, T образуют дополнение в группе G. Для каждого g ∈ G существует единственная пара (s,t) ∈ S × T такая, что g = s t; пусть φ(g) = (s,t) — единственная такая пара, тогда произведение элементов пары равно g.

LaTeX

$$$\forall g \in G\;\exists! (s,t) \in S \times T:\; g = s t.$$$

Lean4

@[simp]
theorem equiv_fst_mul_equiv_snd (g : G) : ↑(hST.equiv g).fst * (hST.equiv g).snd = g :=
  (Equiv.ofBijective (fun x : S × T => x.1.1 * x.2.1) hST).right_inv g

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