bot_or_nontrivial — Mathlib

English

Every submonoid is either the bottom submonoid or nontrivial.

Русский

Каждое подмножество либо равно ⊥, либо не тривиально.

LaTeX

$$$ \forall S : Submonoid M,\ S = \bot \lor Nontrivial S $$$

Lean4

/-- A submonoid is either the trivial submonoid or nontrivial. -/
@[to_additive /-- An additive submonoid is either the trivial additive submonoid or nontrivial. -/
    ]
theorem bot_or_nontrivial (S : Submonoid M) : S = ⊥ ∨ Nontrivial S := by
  simp only [eq_bot_iff_forall, nontrivial_iff_exists_ne_one, ← not_forall, ← Classical.not_imp, Classical.em]

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