isComplement_univ_singleton — Mathlib

English

For every g in G, the pair (Set.univ, {g}) is a complement: univ and singleton form a complement pair.

Русский

Для каждого g ∈ G единичная пара (множество-единица) образует дополнение с единичной группой.

LaTeX

$$$ \forall g:\,G, \text{IsComplement}(\mathrm{univ} , {g}). $$$

Lean4

@[to_additive]
theorem isComplement_univ_singleton {g : G} : IsComplement (univ : Set G) { g } :=
  ⟨fun ⟨_, _, rfl⟩ ⟨_, _, rfl⟩ h => Prod.ext (Subtype.ext (mul_right_cancel h)) rfl, fun x =>
    ⟨⟨⟨x * g⁻¹, ⟨⟩⟩, g, rfl⟩, inv_mul_cancel_right x g⟩⟩

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