subsingleton_of_subsingleton — Mathlib

English

If Subsemigroup M is Subsingleton, then M is Subsingleton.

Русский

Если подполугруппа M является одиночной, то M тоже одиночной.

LaTeX

$$$ [Subsingleton (Subsemigroup M)] \\Rightarrow Subsingleton M $$$

Lean4

@[to_additive]
theorem subsingleton_of_subsingleton [Subsingleton (Subsemigroup M)] : Subsingleton M :=
  by
  constructor; intro x y
  have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
  exact absurd (this x) notMem_bot

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