isComplement_univ_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem isComplement_univ_left : IsComplement univ S ↔ ∃ 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.2.1, a.2.2⟩
  · have : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : Set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
      h.1 ((inv_mul_cancel a).trans (inv_mul_cancel b).symm)
    exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).2
  · rintro ⟨g, rfl⟩
    exact isComplement_univ_singleton

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