isComplement_iff_bijective — Mathlib

English

For SetLike S, T ⊆ G, IsComplement S T iff the map x ↦ x.1 * x.2 from S × T to G is bijective.

Русский

Для подмножеств S, T ⊆ G верно: IsComplement S T эквивалентно биекції x ↦ x.1 x x.2 из S × T в G.

LaTeX

$$$ \text{IsComplement}(S,T) \iff \text{Bijective } (x: S \times T) \mapsto (x.1 : G) \cdot (x.2 : G). $$$

Lean4

/-- The correct way to unfold `IsComplement` for `SetLike`s such as `Subgroup`s -/
@[to_additive /-- The correct way to unfold `IsComplement` for `SetLike`s such as `AddSubgroup`s -/
    ]
theorem isComplement_iff_bijective {S : Type*} [SetLike S G] (s t : S) :
    IsComplement (G := G) s t ↔ Function.Bijective fun x : s × t => (x.1 : G) * (x.2 : G) :=
  Iff.rfl

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