existsUnique — Mathlib

English

Subgroup.IsComplement.existsUnique: If S and T form a complement, then for every g ∈ G there exists a unique x ∈ S × T with x.1.1 * x.2.1 = g.

Русский

Subgroup.IsComplement.existsUnique: если S и T образуют дополнение, то для каждого g ∈ G существует ровно одна пара x ∈ S × T такая, что x.1.1 * x.2.1 = g.

LaTeX

$$$ \text{IsComplement } S T \Rightarrow \forall g:\,G, \exists! x:\, S \times T, x.1.1 \cdot x.2.1 = g. $$$

Lean4

@[to_additive]
theorem existsUnique (h : IsComplement S T) (g : G) : ∃! x : S × T, x.1.1 * x.2.1 = g :=
  isComplement_iff_existsUnique.mp h g

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