isComplement_univ_right — Mathlib

English

IsComplement S Set.univ iff there exists g with S = {g}.

Русский

IsComplement S Set.univ эквивалентно существованию g с S = {g}.

LaTeX

$$$ \text{IsComplement}(S, \mathrm{univ}) \iff \exists g:\,G, S = \{g\}. $$$

Lean4

@[to_additive]
theorem isComplement_univ_right : IsComplement S univ ↔ ∃ g : G, S = { g } :=
  by
  refine ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
  · obtain ⟨a, _⟩ := h.2 1
    exact ⟨a.1.1, a.1.2⟩
  · have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : Set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
      h.1 ((mul_inv_cancel a).trans (mul_inv_cancel b).symm)
    exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).1
  · rintro ⟨g, rfl⟩
    exact isComplement_singleton_univ

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