subsingleton_iff — Mathlib

English

The underlying set of sInf H is the intersection over H.

Русский

Множество, лежащее в основании sInf H, равно ⋂ H.

LaTeX

$$((sInf H : Subgroup G) : Set G) = \bigcap_{S \in H} S$$

Lean4

@[to_additive (attr := simp)]
theorem subsingleton_iff : Subsingleton (Subgroup G) ↔ Subsingleton G :=
  ⟨fun _ =>
    ⟨fun x y =>
      have : ∀ i : G, i = 1 := fun i => mem_bot.mp <| Subsingleton.elim (⊤ : Subgroup G) ⊥ ▸ mem_top i
      (this x).trans (this y).symm⟩,
    fun _ => ⟨fun x y => Subgroup.ext fun i => Subsingleton.elim 1 i ▸ by simp⟩⟩

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