coe_eq_singleton — Mathlib

English

There exists a g with (H : Set G) = {g} iff H = ⊥.

Русский

Существует элемент g такой, что (H : Set G) = {g} тогда и только тогда H = ⊥.

LaTeX

$$$$ (\\exists g:\\, G, (H : \\mathrm{Set}~G) = \\{g\\}) \\iff H = \\bot. $$$$

Lean4

@[to_additive]
theorem coe_eq_singleton {H : Subgroup G} : (∃ g : G, (H : Set G) = { g }) ↔ H = ⊥ :=
  ⟨fun ⟨g, hg⟩ =>
    haveI : Subsingleton (H : Set G) := by
      rw [hg]
      infer_instance
    H.eq_bot_of_subsingleton,
    fun h => ⟨1, SetLike.ext'_iff.mp h⟩⟩

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