nontrivial_iff_exists_ne_one — Mathlib

English

A submonoid is nontrivial if and only if there exists an element in S different from the identity 1_M.

Русский

Подмножество не тривиально тогда и только тогда, когда существует элемент x ∈ S, отличный от единицы 1_M.

LaTeX

$$$ \text{nontrivial\_iff\_exists\_ne\_one} (S) : \mathrm{Nontrivial}(S) \leftrightarrow \exists x \in S, x \neq 1_M$$$

Lean4

@[to_additive]
theorem nontrivial_iff_exists_ne_one (S : Submonoid M) : Nontrivial S ↔ ∃ x ∈ S, x ≠ (1 : M) :=
  calc
    Nontrivial S ↔ ∃ x : S, x ≠ 1 := nontrivial_iff_exists_ne 1
    _ ↔ ∃ (x : _) (hx : x ∈ S), (⟨x, hx⟩ : S) ≠ ⟨1, S.one_mem⟩ := Subtype.exists
    _ ↔ ∃ x ∈ S, x ≠ (1 : M) := by simp [Ne]

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