English
The family of submonoids of M is a subsingleton if and only if M itself is a subsingleton; i.e., Submonoid M is determined completely by the underlying set-theoretic triviality of M.
Русский
Множество подмонойдов M является подселективным тогда и только тогда, когда сам M является подселективным; подмножество монойности полностью определяется свойством M.
LaTeX
$$$\mathrm{Subsingleton}(\mathrm{Submonoid} M) \;\Leftrightarrow\; \mathrm{Subsingleton}(M)$$$
Lean4
@[to_additive (attr := simp)]
theorem subsingleton_iff : Subsingleton (Submonoid M) ↔ Subsingleton M :=
⟨fun _ =>
⟨fun x y =>
have : ∀ i : M, i = 1 := fun i => mem_bot.mp <| Subsingleton.elim (⊤ : Submonoid M) ⊥ ▸ mem_top i
(this x).trans (this y).symm⟩,
fun _ => ⟨fun x y => Submonoid.ext fun i => Subsingleton.elim 1 i ▸ by simp⟩⟩
