exists_one_lt' — Mathlib

English

There exists an element a with 1 < a in any nontrivial ordered group.

Русский

Существует элемент a с 1 < a в любой ненулевой упорядоченной группе.

LaTeX

$$$\exists a\; (1 < a)$$$

Lean4

@[to_additive exists_zero_lt]
theorem exists_one_lt' [Nontrivial α] : ∃ a : α, 1 < a :=
  by
  obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)
  obtain h | h := hy.lt_or_gt
  · exact ⟨y⁻¹, one_lt_inv'.mpr h⟩
  ·
    exact
      ⟨y, h⟩
        -- see Note [lower instance priority]

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