isComplement_iff_existsUnique — Mathlib

English

IsComplement S T is equivalent to: for every g ∈ G there exists a unique pair (s,t) ∈ S × T with s t = g.

Русский

IsComplement S T эквивалентно тому, что для каждого g ∈ G существует уникальная пара (s,t) ∈ S × T с s t = g.

LaTeX

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

Lean4

@[to_additive]
theorem isComplement_iff_existsUnique : IsComplement S T ↔ ∀ g : G, ∃! x : S × T, x.1.1 * x.2.1 = g :=
  Function.bijective_iff_existsUnique _

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