isComplement_singleton_univ — Mathlib

English

For every g in G, IsComplement ({g} : Set G) univ.

Русский

Для каждого g ∈ G, {g} образует дополнение с Set.univ.

LaTeX

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

Lean4

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

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